]> git.pld-linux.org Git - packages/coq.git/blob - coq.spec
- this version relies on fpmath=sse, so require sse2 on x86
[packages/coq.git] / coq.spec
1 #
2 # Conditional build:
3 %bcond_without  ocaml_opt       # native optimized binaries (bytecode is always built)
4 %bcond_without  sse2            # SSE2 instructions (i387 maths not supported as of 8.15)
5 %bcond_with     doc             # documentation
6 %bcond_with     tests           # run testsuite (csdp dependant micromega tests fail badly on x86_64)
7 #
8 %ifarch pentium4 %{x8664} x32
9 %define         with_sse2       1
10 %endif
11
12 %ifnarch %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
13 %undefine       with_ocaml_opt
14 %endif
15
16 Summary:        The Coq Proof Assistant
17 Summary(pl.UTF-8):      Coq - narzędzie pomagające w udowadnianiu
18 Name:           coq
19 Version:        8.15.0
20 Release:        1
21 License:        LGPL v2.1
22 Group:          Applications/Math
23 #Source0Download: https://github.com/coq/coq/releases
24 Source0:        https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz
25 # Source0-md5:  cfa91d270e013b0ebe49120c2101d010
26 Source1:        coqide.desktop
27 Source2:        coqide.xpm
28 Patch0:         %{name}-dune-prefix.patch
29 URL:            https://coq.inria.fr/
30 BuildRequires:  bash
31 BuildRequires:  ocaml >= 1:4.05
32 BuildRequires:  camlp5 >= 5.01
33 BuildRequires:  ocaml-dune >= 2.5.0
34 BuildRequires:  ocaml-findlib >= 1.8.1
35 BuildRequires:  ocaml-zarith-devel >= 1.10
36 BuildRequires:  ocaml-lablgtk3-devel >= 3.1.0
37 BuildRequires:  ocaml-lablgtk3-gtksourceview-devel >= 3.1.0
38 BuildRequires:  sed >= 4.0
39 %if %{with doc}
40 BuildRequires:  python3 >= 1:3
41 # TODO (and adjust package name)
42 BuildRequires:  python3-antlr4-python3-runtime >= 4.7.1
43 BuildRequires:  python3-bs4 >= 4.0.6
44 BuildRequires:  python3-pexpect >= 4.2.1
45 BuildRequires:  python3-sphinx_rtd_theme >= 0.4.3
46 # TODO (and adjust package name)
47 BuildRequires:  python3-sphinxcontrib-bibtex >= 0.4.2
48 BuildRequires:  sphinx-pdg >= 2.3.1
49 # TODO: update texlive packages list (or drop pdf building leaving only html)
50 BuildRequires:  texlive-fonts-cmextra
51 BuildRequires:  texlive-fonts-cmsuper
52 BuildRequires:  texlive-fonts-other
53 BuildRequires:  texlive-format-pdflatex
54 BuildRequires:  texlive-latex-ams
55 BuildRequires:  texlive-latex-comment
56 BuildRequires:  texlive-latex-moreverb
57 BuildRequires:  texlive-latex-ucs
58 BuildRequires:  texlive-makeindex
59 BuildRequires:  texlive-psutils
60 # hyperref.sty (from latex) requires ifxexex.sty (from xetex)
61 BuildRequires:  texlive-xetex
62 %endif
63 %if %{with sse2}
64 Requires:       cpuinfo(sse2)
65 %endif
66 Requires:       ocaml-coq-devel = %{version}-%{release}
67 Obsoletes:      coq-emacs < 8.13.1
68 # same as ocaml-zarith
69 ExclusiveArch:  %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
70 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
71
72 # Exclude private ocaml interfaces
73 %define         _noautoreq      ocamlx?\\\((Configwin_types|Interface|Richpp|Serialize|Xml_p(arser|rinter)|Xmlprotocol)\\\)
74
75 %description
76 Coq is a proof assistant which:
77  - allows to handle calculus assertions,
78  - check mechanically proofs of these assertions,
79  - helps to find formal proofs,
80  - extracts a certified program from the constructive proof of its
81    formal specification.
82
83 %description -l pl.UTF-8
84 Coq to narzędzie pomagające w udowadnianiu, które:
85 - pozwala uporać się z twierdzeniami dotyczącymi rachunku
86   różniczkowego,
87 - mechanicznie sprawdzać dowody tych twierdzeń,
88 - pomagać w znalezieniu formalnych dowodów,
89 - wyciągać program o dowiedzionej poprawności z konstruktywnego dowodu
90   jego formalnej specyfikacji.
91
92 %package -n ocaml-coq
93 Summary:        Coq Proof Assistant - OCaml runtime libraries
94 Summary(pl.UTF-8):      Asystent udowadniania Coq - biblioteki uruchomieniowe OCamla
95 Group:          Libraries
96 %requires_eq    ocaml-runtime
97
98 %description -n ocaml-coq
99 Coq Proof Assistant - OCaml runtime libraries.
100
101 %description -n ocaml-coq -l pl.UTF-8
102 Asystent udowadniania Coq - biblioteki uruchomieniowe OCamla.
103
104 %package -n ocaml-coq-devel
105 Summary:        Coq Proof Assistant - OCaml development libraries
106 Summary(pl.UTF-8):      Asystent udowadniania Coq - biblioteki programistyczne OCamla
107 Group:          Development/Libraries
108 Requires:       ocaml-coq = %{version}-%{release}
109 %requires_eq    ocaml
110
111 %description -n ocaml-coq-devel
112 Coq Proof Assistant - OCaml development libraries.
113
114 %description -n ocaml-coq-devel -l pl.UTF-8
115 Asystent udowadniania Coq - biblioteki programistyczne OCamla.
116
117 %package latex
118 Summary:        Coq documentation style for LaTeX
119 Summary(pl.UTF-8):      Styl dokumentacji Coq dla LaTeXa
120 Group:          Development/Tools
121 Requires:       %{name} = %{version}-%{release}
122
123 %description latex
124 Coq documentation style for LaTeX.
125
126 %description latex -l pl.UTF-8
127 Styl dokumentacji Coq dla LaTeXa.
128
129 %prep
130 %setup -q
131 %patch0 -p1
132
133 %{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' tools/configure/configure.ml
134 %if %{without sse2}
135 %{__sed} -i -e '/cflags_sse2/ s/-msse2 -mfpmath=sse//' tools/configure/configure.ml
136 %endif
137 %{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in
138
139 %{__sed} -i -e '1s,/usr/bin/env python3,%{__python3},' \
140       tools/make-both-single-timing-files.py \
141       tools/make-both-time-files.py \
142       tools/make-one-time-file.py
143
144 %{__sed} -i -e '1s,/usr/bin/env python2,%{__python3},' \
145       doc/tools/coqrst/notations/fontsupport.py
146
147 %build
148 ./configure \
149         -prefix %{_prefix} \
150         -configdir %{_sysconfdir}/%{name} \
151         -datadir %{_datadir}/%{name} \
152         -docdir %{_docdir}/%{name}-%{version} \
153         -libdir %{_libdir}/coq \
154         -mandir %{_mandir} \
155 %if %{with ocaml_opt}
156         -coqide opt \
157         -native-compiler yes \
158 %else
159         -byte-only \
160         -coqide byte \
161         -native-compiler no \
162 %endif
163         -browser "xdg-open %s" \
164         %{?with_doc:-with-doc yes}
165
166 %{__make} world \
167         CAML_LD_LIBRARY_PATH=kernel/byterun \
168         _DDISPLAY=verbose \
169         VERBOSE=1
170 %{?with_tests:%{__make} check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories
171
172 %install
173 rm -rf $RPM_BUILD_ROOT
174 install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir},%{_sysconfdir}/%{name}}
175
176 %{__make} install \
177         _DDISPLAY=verbose \
178         DESTDIR=$RPM_BUILD_ROOT
179
180 cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir}
181 cp -p %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir}
182
183 cp -p CREDITS README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}
184
185 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*.ml
186 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*/*.ml
187 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*/*/*.ml
188 %{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coqide-server/*/*.ml
189 # build time
190 %{__rm} -r $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/tools
191
192 %clean
193 rm -rf $RPM_BUILD_ROOT
194
195 %files
196 %defattr(644,root,root,755)
197 %doc %{_docdir}/%{name}-%{version}
198 %dir %{_sysconfdir}/%{name}
199 %attr(755,root,root) %{_bindir}/coq-tex
200 %attr(755,root,root) %{_bindir}/coq_makefile
201 %attr(755,root,root) %{_bindir}/coqc
202 %attr(755,root,root) %{_bindir}/coqc.byte
203 %attr(755,root,root) %{_bindir}/coqchk
204 %attr(755,root,root) %{_bindir}/coqdep
205 %attr(755,root,root) %{_bindir}/coqdoc
206 %attr(755,root,root) %{_bindir}/coqide
207 %attr(755,root,root) %{_bindir}/coqidetop.byte
208 %attr(755,root,root) %{_bindir}/coqidetop.opt
209 %attr(755,root,root) %{_bindir}/coqnative
210 %attr(755,root,root) %{_bindir}/coqpp
211 %attr(755,root,root) %{_bindir}/coqproofworker.opt
212 %attr(755,root,root) %{_bindir}/coqqueryworker.opt
213 %attr(755,root,root) %{_bindir}/coqtacticworker.opt
214 %attr(755,root,root) %{_bindir}/coqtop
215 %attr(755,root,root) %{_bindir}/coqtop.byte
216 %attr(755,root,root) %{_bindir}/coqtop.opt
217 %attr(755,root,root) %{_bindir}/coqwc
218 %attr(755,root,root) %{_bindir}/coqworkmgr
219 %attr(755,root,root) %{_bindir}/csdpcert
220 %attr(755,root,root) %{_bindir}/ocamllibdep
221 %attr(755,root,root) %{_bindir}/votour
222 %dir %{_libdir}/coq
223 %{_libdir}/coq/theories
224 %{_libdir}/coq/user-contrib
225 %{_mandir}/man1/coq_makefile.1*
226 %{_mandir}/man1/coq-tex.1*
227 %{_mandir}/man1/coqc.1*
228 %{_mandir}/man1/coqchk.1*
229 %{_mandir}/man1/coqdep.1*
230 %{_mandir}/man1/coqdoc.1*
231 %{_mandir}/man1/coqide.1*
232 %{_mandir}/man1/coqnative.1*
233 %{_mandir}/man1/coqtop.1*
234 %{_mandir}/man1/coqtop.byte.1*
235 %{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*}
236 %{_mandir}/man1/coqwc.1*
237 %{_desktopdir}/coqide.desktop
238 %{_pixmapsdir}/coqide.xpm
239 %{_datadir}/%{name}
240
241 %files -n ocaml-coq
242 %defattr(644,root,root,755)
243 %dir %{_libdir}/ocaml/coq-core
244 %{_libdir}/ocaml/coq-core/META
245 %{_libdir}/ocaml/coq-core/revision
246 %dir %{_libdir}/ocaml/coq-core/boot
247 %{_libdir}/ocaml/coq-core/boot/*.cma
248 %dir %{_libdir}/ocaml/coq-core/clib
249 %{_libdir}/ocaml/coq-core/clib/*.cma
250 %dir %{_libdir}/ocaml/coq-core/config
251 %{_libdir}/ocaml/coq-core/config/*.cma
252 %dir %{_libdir}/ocaml/coq-core/engine
253 %{_libdir}/ocaml/coq-core/engine/*.cma
254 %dir %{_libdir}/ocaml/coq-core/gramlib
255 %{_libdir}/ocaml/coq-core/gramlib/*.cma
256 %dir %{_libdir}/ocaml/coq-core/interp
257 %{_libdir}/ocaml/coq-core/interp/*.cma
258 %dir %{_libdir}/ocaml/coq-core/kernel
259 %{_libdir}/ocaml/coq-core/kernel/*.cma
260 %dir %{_libdir}/ocaml/coq-core/lib
261 %{_libdir}/ocaml/coq-core/lib/*.cma
262 %dir %{_libdir}/ocaml/coq-core/library
263 %{_libdir}/ocaml/coq-core/library/*.cma
264 %dir %{_libdir}/ocaml/coq-core/parsing
265 %{_libdir}/ocaml/coq-core/parsing/*.cma
266 %dir %{_libdir}/ocaml/coq-core/plugins
267 %dir %{_libdir}/ocaml/coq-core/plugins/btauto
268 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cma
269 %dir %{_libdir}/ocaml/coq-core/plugins/cc
270 %{_libdir}/ocaml/coq-core/plugins/cc/*.cma
271 %dir %{_libdir}/ocaml/coq-core/plugins/derive
272 %{_libdir}/ocaml/coq-core/plugins/derive/*.cma
273 %dir %{_libdir}/ocaml/coq-core/plugins/extraction
274 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cma
275 %dir %{_libdir}/ocaml/coq-core/plugins/firstorder
276 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cma
277 %dir %{_libdir}/ocaml/coq-core/plugins/funind
278 %{_libdir}/ocaml/coq-core/plugins/funind/*.cma
279 %dir %{_libdir}/ocaml/coq-core/plugins/ltac
280 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cma
281 %dir %{_libdir}/ocaml/coq-core/plugins/ltac2
282 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cma
283 %dir %{_libdir}/ocaml/coq-core/plugins/micromega
284 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cma
285 %dir %{_libdir}/ocaml/coq-core/plugins/nsatz
286 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cma
287 %dir %{_libdir}/ocaml/coq-core/plugins/number_string_notation
288 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cma
289 %dir %{_libdir}/ocaml/coq-core/plugins/ring
290 %{_libdir}/ocaml/coq-core/plugins/ring/*.cma
291 %dir %{_libdir}/ocaml/coq-core/plugins/rtauto
292 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cma
293 %dir %{_libdir}/ocaml/coq-core/plugins/ssreflect
294 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cma
295 %dir %{_libdir}/ocaml/coq-core/plugins/ssrmatching
296 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cma
297 %dir %{_libdir}/ocaml/coq-core/plugins/tauto
298 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cma
299 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial
300 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p0
301 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cma
302 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p1
303 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cma
304 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p2
305 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cma
306 %dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p3
307 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cma
308 %dir %{_libdir}/ocaml/coq-core/plugins/zify
309 %{_libdir}/ocaml/coq-core/plugins/zify/*.cma
310 %dir %{_libdir}/ocaml/coq-core/pretyping
311 %{_libdir}/ocaml/coq-core/pretyping/*.cma
312 %dir %{_libdir}/ocaml/coq-core/printing
313 %{_libdir}/ocaml/coq-core/printing/*.cma
314 %dir %{_libdir}/ocaml/coq-core/proofs
315 %{_libdir}/ocaml/coq-core/proofs/*.cma
316 %dir %{_libdir}/ocaml/coq-core/stm
317 %{_libdir}/ocaml/coq-core/stm/*.cma
318 %dir %{_libdir}/ocaml/coq-core/sysinit
319 %{_libdir}/ocaml/coq-core/sysinit/*.cma
320 %dir %{_libdir}/ocaml/coq-core/tactics
321 %{_libdir}/ocaml/coq-core/tactics/*.cma
322 %dir %{_libdir}/ocaml/coq-core/top_printers
323 %{_libdir}/ocaml/coq-core/top_printers/*.cma
324 %dir %{_libdir}/ocaml/coq-core/toplevel
325 %{_libdir}/ocaml/coq-core/toplevel/*.cma
326 %dir %{_libdir}/ocaml/coq-core/vernac
327 %{_libdir}/ocaml/coq-core/vernac/*.cma
328 %dir %{_libdir}/ocaml/coq-core/vm
329 %{_libdir}/ocaml/coq-core/vm/*.cma
330 %dir %{_libdir}/ocaml/coqide
331 %{_libdir}/ocaml/coqide/META
332 %dir %{_libdir}/ocaml/coqide-server
333 %{_libdir}/ocaml/coqide-server/META
334 %dir %{_libdir}/ocaml/coqide-server/core
335 %{_libdir}/ocaml/coqide-server/core/*.cma
336 %dir %{_libdir}/ocaml/coqide-server/protocol
337 %{_libdir}/ocaml/coqide-server/protocol/*.cma
338 %if %{with ocaml_opt}
339 %attr(755,root,root) %{_libdir}/ocaml/coq-core/boot/*.cmxs
340 %attr(755,root,root) %{_libdir}/ocaml/coq-core/clib/*.cmxs
341 %attr(755,root,root) %{_libdir}/ocaml/coq-core/config/*.cmxs
342 %attr(755,root,root) %{_libdir}/ocaml/coq-core/engine/*.cmxs
343 %attr(755,root,root) %{_libdir}/ocaml/coq-core/gramlib/*.cmxs
344 %attr(755,root,root) %{_libdir}/ocaml/coq-core/interp/*.cmxs
345 %attr(755,root,root) %{_libdir}/ocaml/coq-core/kernel/*.cmxs
346 %attr(755,root,root) %{_libdir}/ocaml/coq-core/lib/*.cmxs
347 %attr(755,root,root) %{_libdir}/ocaml/coq-core/library/*.cmxs
348 %attr(755,root,root) %{_libdir}/ocaml/coq-core/parsing/*.cmxs
349 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmxs
350 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/cc/*.cmxs
351 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/derive/*.cmxs
352 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmxs
353 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmxs
354 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/funind/*.cmxs
355 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmxs
356 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmxs
357 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmxs
358 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmxs
359 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmxs
360 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ring/*.cmxs
361 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmxs
362 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmxs
363 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmxs
364 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmxs
365 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmxs
366 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmxs
367 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmxs
368 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmxs
369 %attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/zify/*.cmxs
370 %attr(755,root,root) %{_libdir}/ocaml/coq-core/pretyping/*.cmxs
371 %attr(755,root,root) %{_libdir}/ocaml/coq-core/printing/*.cmxs
372 %attr(755,root,root) %{_libdir}/ocaml/coq-core/proofs/*.cmxs
373 %attr(755,root,root) %{_libdir}/ocaml/coq-core/stm/*.cmxs
374 %attr(755,root,root) %{_libdir}/ocaml/coq-core/sysinit/*.cmxs
375 %attr(755,root,root) %{_libdir}/ocaml/coq-core/tactics/*.cmxs
376 %attr(755,root,root) %{_libdir}/ocaml/coq-core/top_printers/*.cmxs
377 %attr(755,root,root) %{_libdir}/ocaml/coq-core/toplevel/*.cmxs
378 %attr(755,root,root) %{_libdir}/ocaml/coq-core/vernac/*.cmxs
379 %attr(755,root,root) %{_libdir}/ocaml/coq-core/vm/*.cmxs
380 %attr(755,root,root) %{_libdir}/ocaml/coqide-server/core/*.cmxs
381 %attr(755,root,root) %{_libdir}/ocaml/coqide-server/protocol/*.cmxs
382 %endif
383 %attr(755,root,root) %{_libdir}/ocaml/stublibs/dllcoqrun_stubs.so
384
385 %files -n ocaml-coq-devel
386 %defattr(644,root,root,755)
387 %{_libdir}/ocaml/coq-core/dune-package
388 %{_libdir}/ocaml/coq-core/opam
389 %{_libdir}/ocaml/coq-core/boot/*.cmi
390 %{_libdir}/ocaml/coq-core/boot/*.cmt
391 %{_libdir}/ocaml/coq-core/boot/*.cmti
392 %{_libdir}/ocaml/coq-core/boot/*.mli
393 %{_libdir}/ocaml/coq-core/clib/*.cmi
394 %{_libdir}/ocaml/coq-core/clib/*.cmt
395 %{_libdir}/ocaml/coq-core/clib/*.cmti
396 %{_libdir}/ocaml/coq-core/clib/*.mli
397 %{_libdir}/ocaml/coq-core/config/*.cmi
398 %{_libdir}/ocaml/coq-core/config/*.cmt
399 %{_libdir}/ocaml/coq-core/config/*.cmti
400 %{_libdir}/ocaml/coq-core/config/*.mli
401 %{_libdir}/ocaml/coq-core/engine/*.cmi
402 %{_libdir}/ocaml/coq-core/engine/*.cmt
403 %{_libdir}/ocaml/coq-core/engine/*.cmti
404 %{_libdir}/ocaml/coq-core/engine/*.mli
405 %{_libdir}/ocaml/coq-core/gramlib/*.cmi
406 %{_libdir}/ocaml/coq-core/gramlib/*.cmt
407 %{_libdir}/ocaml/coq-core/gramlib/*.cmti
408 %{_libdir}/ocaml/coq-core/gramlib/*.mli
409 %{_libdir}/ocaml/coq-core/interp/*.cmi
410 %{_libdir}/ocaml/coq-core/interp/*.cmt
411 %{_libdir}/ocaml/coq-core/interp/*.cmti
412 %{_libdir}/ocaml/coq-core/interp/*.mli
413 %{_libdir}/ocaml/coq-core/kernel/*.cmi
414 %{_libdir}/ocaml/coq-core/kernel/*.cmt
415 %{_libdir}/ocaml/coq-core/kernel/*.cmti
416 %{_libdir}/ocaml/coq-core/kernel/*.mli
417 %{_libdir}/ocaml/coq-core/lib/*.cmi
418 %{_libdir}/ocaml/coq-core/lib/*.cmt
419 %{_libdir}/ocaml/coq-core/lib/*.cmti
420 %{_libdir}/ocaml/coq-core/lib/*.mli
421 %{_libdir}/ocaml/coq-core/library/*.cmi
422 %{_libdir}/ocaml/coq-core/library/*.cmt
423 %{_libdir}/ocaml/coq-core/library/*.cmti
424 %{_libdir}/ocaml/coq-core/library/*.mli
425 %{_libdir}/ocaml/coq-core/parsing/*.cmi
426 %{_libdir}/ocaml/coq-core/parsing/*.cmt
427 %{_libdir}/ocaml/coq-core/parsing/*.cmti
428 %{_libdir}/ocaml/coq-core/parsing/*.mli
429 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmi
430 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmt
431 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmti
432 %{_libdir}/ocaml/coq-core/plugins/btauto/*.mli
433 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmi
434 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmt
435 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmti
436 %{_libdir}/ocaml/coq-core/plugins/cc/*.mli
437 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmi
438 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmt
439 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmti
440 %{_libdir}/ocaml/coq-core/plugins/derive/*.mli
441 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmi
442 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmt
443 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmti
444 %{_libdir}/ocaml/coq-core/plugins/extraction/*.mli
445 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmi
446 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmt
447 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmti
448 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.mli
449 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmi
450 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmt
451 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmti
452 %{_libdir}/ocaml/coq-core/plugins/funind/*.mli
453 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmi
454 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmt
455 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmti
456 %{_libdir}/ocaml/coq-core/plugins/ltac/*.mli
457 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmi
458 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmt
459 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmti
460 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.mli
461 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmi
462 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmt
463 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmti
464 %{_libdir}/ocaml/coq-core/plugins/micromega/*.mli
465 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmi
466 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmt
467 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmti
468 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.mli
469 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmi
470 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmt
471 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmti
472 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.mli
473 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmi
474 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmt
475 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmti
476 %{_libdir}/ocaml/coq-core/plugins/ring/*.mli
477 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmi
478 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmt
479 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmti
480 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.mli
481 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmi
482 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmt
483 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmti
484 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.mli
485 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmi
486 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmt
487 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmti
488 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.mli
489 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmi
490 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmt
491 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmti
492 %{_libdir}/ocaml/coq-core/plugins/tauto/*.mli
493 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmi
494 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmt
495 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmti
496 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.mli
497 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmi
498 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmt
499 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmti
500 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.mli
501 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmi
502 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmt
503 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmti
504 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.mli
505 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmi
506 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmt
507 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmti
508 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.mli
509 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmi
510 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmt
511 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmti
512 %{_libdir}/ocaml/coq-core/plugins/zify/*.mli
513 %{_libdir}/ocaml/coq-core/pretyping/*.cmi
514 %{_libdir}/ocaml/coq-core/pretyping/*.cmt
515 %{_libdir}/ocaml/coq-core/pretyping/*.cmti
516 %{_libdir}/ocaml/coq-core/pretyping/*.mli
517 %{_libdir}/ocaml/coq-core/printing/*.cmi
518 %{_libdir}/ocaml/coq-core/printing/*.cmt
519 %{_libdir}/ocaml/coq-core/printing/*.cmti
520 %{_libdir}/ocaml/coq-core/printing/*.mli
521 %{_libdir}/ocaml/coq-core/proofs/*.cmi
522 %{_libdir}/ocaml/coq-core/proofs/*.cmt
523 %{_libdir}/ocaml/coq-core/proofs/*.cmti
524 %{_libdir}/ocaml/coq-core/proofs/*.mli
525 %{_libdir}/ocaml/coq-core/stm/*.cmi
526 %{_libdir}/ocaml/coq-core/stm/*.cmt
527 %{_libdir}/ocaml/coq-core/stm/*.cmti
528 %{_libdir}/ocaml/coq-core/stm/*.mli
529 %{_libdir}/ocaml/coq-core/sysinit/*.cmi
530 %{_libdir}/ocaml/coq-core/sysinit/*.cmt
531 %{_libdir}/ocaml/coq-core/sysinit/*.cmti
532 %{_libdir}/ocaml/coq-core/sysinit/*.mli
533 %{_libdir}/ocaml/coq-core/tactics/*.cmi
534 %{_libdir}/ocaml/coq-core/tactics/*.cmt
535 %{_libdir}/ocaml/coq-core/tactics/*.cmti
536 %{_libdir}/ocaml/coq-core/tactics/*.mli
537 %{_libdir}/ocaml/coq-core/top_printers/*.cmi
538 %{_libdir}/ocaml/coq-core/top_printers/*.cmt
539 %{_libdir}/ocaml/coq-core/top_printers/*.cmti
540 %{_libdir}/ocaml/coq-core/top_printers/*.mli
541 %{_libdir}/ocaml/coq-core/toplevel/*.cmi
542 %{_libdir}/ocaml/coq-core/toplevel/*.cmt
543 %{_libdir}/ocaml/coq-core/toplevel/*.cmti
544 %{_libdir}/ocaml/coq-core/toplevel/*.mli
545 %{_libdir}/ocaml/coq-core/vernac/*.cmi
546 %{_libdir}/ocaml/coq-core/vernac/*.cmt
547 %{_libdir}/ocaml/coq-core/vernac/*.cmti
548 %{_libdir}/ocaml/coq-core/vernac/*.mli
549 %{_libdir}/ocaml/coq-core/vm/libcoqrun_stubs.a
550 %{_libdir}/ocaml/coq-core/vm/*.cmi
551 %{_libdir}/ocaml/coq-core/vm/*.cmt
552 %{_libdir}/ocaml/coqide/dune-package
553 %{_libdir}/ocaml/coqide/opam
554 %{_libdir}/ocaml/coqide-server/dune-package
555 %{_libdir}/ocaml/coqide-server/opam
556 %{_libdir}/ocaml/coqide-server/core/*.cmi
557 %{_libdir}/ocaml/coqide-server/core/*.cmt
558 %{_libdir}/ocaml/coqide-server/core/*.cmti
559 %{_libdir}/ocaml/coqide-server/core/*.mli
560 %{_libdir}/ocaml/coqide-server/protocol/*.cmi
561 %{_libdir}/ocaml/coqide-server/protocol/*.cmt
562 %{_libdir}/ocaml/coqide-server/protocol/*.cmti
563 %{_libdir}/ocaml/coqide-server/protocol/*.mli
564 %if %{with ocaml_opt}
565 %{_libdir}/ocaml/coq-core/boot/boot.a
566 %{_libdir}/ocaml/coq-core/boot/*.cmx
567 %{_libdir}/ocaml/coq-core/boot/*.cmxa
568 %{_libdir}/ocaml/coq-core/clib/clib.a
569 %{_libdir}/ocaml/coq-core/clib/*.cmx
570 %{_libdir}/ocaml/coq-core/clib/*.cmxa
571 %{_libdir}/ocaml/coq-core/config/config.a
572 %{_libdir}/ocaml/coq-core/config/*.cmx
573 %{_libdir}/ocaml/coq-core/config/*.cmxa
574 %{_libdir}/ocaml/coq-core/engine/engine.a
575 %{_libdir}/ocaml/coq-core/engine/*.cmx
576 %{_libdir}/ocaml/coq-core/engine/*.cmxa
577 %{_libdir}/ocaml/coq-core/gramlib/gramlib.a
578 %{_libdir}/ocaml/coq-core/gramlib/*.cmx
579 %{_libdir}/ocaml/coq-core/gramlib/*.cmxa
580 %{_libdir}/ocaml/coq-core/interp/interp.a
581 %{_libdir}/ocaml/coq-core/interp/*.cmx
582 %{_libdir}/ocaml/coq-core/interp/*.cmxa
583 %{_libdir}/ocaml/coq-core/kernel/kernel.a
584 %{_libdir}/ocaml/coq-core/kernel/*.cmx
585 %{_libdir}/ocaml/coq-core/kernel/*.cmxa
586 %{_libdir}/ocaml/coq-core/lib/lib.a
587 %{_libdir}/ocaml/coq-core/lib/*.cmx
588 %{_libdir}/ocaml/coq-core/lib/*.cmxa
589 %{_libdir}/ocaml/coq-core/library/library.a
590 %{_libdir}/ocaml/coq-core/library/*.cmx
591 %{_libdir}/ocaml/coq-core/library/*.cmxa
592 %{_libdir}/ocaml/coq-core/parsing/parsing.a
593 %{_libdir}/ocaml/coq-core/parsing/*.cmx
594 %{_libdir}/ocaml/coq-core/parsing/*.cmxa
595 %{_libdir}/ocaml/coq-core/plugins/btauto/btauto_plugin.a
596 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmx
597 %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmxa
598 %{_libdir}/ocaml/coq-core/plugins/cc/cc_plugin.a
599 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmx
600 %{_libdir}/ocaml/coq-core/plugins/cc/*.cmxa
601 %{_libdir}/ocaml/coq-core/plugins/derive/derive_plugin.a
602 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmx
603 %{_libdir}/ocaml/coq-core/plugins/derive/*.cmxa
604 %{_libdir}/ocaml/coq-core/plugins/extraction/extraction_plugin.a
605 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmx
606 %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmxa
607 %{_libdir}/ocaml/coq-core/plugins/firstorder/firstorder_plugin.a
608 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmx
609 %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmxa
610 %{_libdir}/ocaml/coq-core/plugins/funind/funind_plugin.a
611 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmx
612 %{_libdir}/ocaml/coq-core/plugins/funind/*.cmxa
613 %{_libdir}/ocaml/coq-core/plugins/ltac/ltac_plugin.a
614 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmx
615 %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmxa
616 %{_libdir}/ocaml/coq-core/plugins/ltac2/ltac2_plugin.a
617 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmx
618 %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmxa
619 %{_libdir}/ocaml/coq-core/plugins/micromega/micromega_plugin.a
620 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmx
621 %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmxa
622 %{_libdir}/ocaml/coq-core/plugins/nsatz/nsatz_plugin.a
623 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmx
624 %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmxa
625 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/number_string_notation_plugin.a
626 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmx
627 %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmxa
628 %{_libdir}/ocaml/coq-core/plugins/ring/ring_plugin.a
629 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmx
630 %{_libdir}/ocaml/coq-core/plugins/ring/*.cmxa
631 %{_libdir}/ocaml/coq-core/plugins/rtauto/rtauto_plugin.a
632 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmx
633 %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmxa
634 %{_libdir}/ocaml/coq-core/plugins/ssreflect/ssreflect_plugin.a
635 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmx
636 %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmxa
637 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/ssrmatching_plugin.a
638 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmx
639 %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmxa
640 %{_libdir}/ocaml/coq-core/plugins/tauto/tauto_plugin.a
641 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmx
642 %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmxa
643 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/tuto0_plugin.a
644 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmx
645 %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmxa
646 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/tuto1_plugin.a
647 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmx
648 %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmxa
649 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/tuto2_plugin.a
650 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmx
651 %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmxa
652 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/tuto3_plugin.a
653 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmx
654 %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmxa
655 %{_libdir}/ocaml/coq-core/plugins/zify/zify_plugin.a
656 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmx
657 %{_libdir}/ocaml/coq-core/plugins/zify/*.cmxa
658 %{_libdir}/ocaml/coq-core/pretyping/pretyping.a
659 %{_libdir}/ocaml/coq-core/pretyping/*.cmx
660 %{_libdir}/ocaml/coq-core/pretyping/*.cmxa
661 %{_libdir}/ocaml/coq-core/printing/printing.a
662 %{_libdir}/ocaml/coq-core/printing/*.cmx
663 %{_libdir}/ocaml/coq-core/printing/*.cmxa
664 %{_libdir}/ocaml/coq-core/proofs/proofs.a
665 %{_libdir}/ocaml/coq-core/proofs/*.cmx
666 %{_libdir}/ocaml/coq-core/proofs/*.cmxa
667 %{_libdir}/ocaml/coq-core/stm/stm.a
668 %{_libdir}/ocaml/coq-core/stm/*.cmx
669 %{_libdir}/ocaml/coq-core/stm/*.cmxa
670 %{_libdir}/ocaml/coq-core/sysinit/sysinit.a
671 %{_libdir}/ocaml/coq-core/sysinit/*.cmx
672 %{_libdir}/ocaml/coq-core/sysinit/*.cmxa
673 %{_libdir}/ocaml/coq-core/tactics/tactics.a
674 %{_libdir}/ocaml/coq-core/tactics/*.cmx
675 %{_libdir}/ocaml/coq-core/tactics/*.cmxa
676 %{_libdir}/ocaml/coq-core/top_printers/top_printers.a
677 %{_libdir}/ocaml/coq-core/top_printers/*.cmx
678 %{_libdir}/ocaml/coq-core/top_printers/*.cmxa
679 %{_libdir}/ocaml/coq-core/toplevel/toplevel.a
680 %{_libdir}/ocaml/coq-core/toplevel/*.cmx
681 %{_libdir}/ocaml/coq-core/toplevel/*.cmxa
682 %{_libdir}/ocaml/coq-core/vernac/vernac.a
683 %{_libdir}/ocaml/coq-core/vernac/*.cmx
684 %{_libdir}/ocaml/coq-core/vernac/*.cmxa
685 %{_libdir}/ocaml/coq-core/vm/coqrun.a
686 %{_libdir}/ocaml/coq-core/vm/*.cmx
687 %{_libdir}/ocaml/coq-core/vm/*.cmxa
688 %{_libdir}/ocaml/coqide-server/core/core.a
689 %{_libdir}/ocaml/coqide-server/core/*.cmx
690 %{_libdir}/ocaml/coqide-server/core/*.cmxa
691 %{_libdir}/ocaml/coqide-server/protocol/protocol.a
692 %{_libdir}/ocaml/coqide-server/protocol/*.cmx
693 %{_libdir}/ocaml/coqide-server/protocol/*.cmxa
694 %endif
695
696 %files latex
697 %defattr(644,root,root,755)
698 %{_datadir}/texmf/tex/latex/misc/coqdoc.sty
This page took 0.190666 seconds and 3 git commands to generate.