]>
Commit | Line | Data |
---|---|---|
8f33d8d4 JR |
1 | # |
2 | # Conditional build: | |
10fd38a7 JB |
3 | %bcond_without ocaml_opt # native optimized binaries (bytecode is always built) |
4 | %bcond_with sse2 # SSE2 instructions | |
5 | %bcond_with doc # documentation | |
48226845 | 6 | %bcond_with tests # run testsuite (csdp dependant micromega tests fail badly on x86_64) |
8f33d8d4 | 7 | # |
10fd38a7 JB |
8 | %ifarch pentium4 %{x8664} x32 |
9 | %define with_sse2 1 | |
10 | %endif | |
11 | ||
39bb0263 | 12 | %ifnarch %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 |
48226845 JR |
13 | %undefine with_ocaml_opt |
14 | %endif | |
15 | ||
521adcea | 16 | Summary: The Coq Proof Assistant |
374d5475 | 17 | Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu |
680764bb | 18 | Name: coq |
672cbc20 JB |
19 | Version: 8.15.0 |
20 | Release: 1 | |
83437006 | 21 | License: LGPL v2.1 |
680764bb | 22 | Group: Applications/Math |
672cbc20 | 23 | #Source0Download: https://github.com/coq/coq/releases |
b2cb8983 | 24 | Source0: https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz |
672cbc20 | 25 | # Source0-md5: cfa91d270e013b0ebe49120c2101d010 |
8bee228d JR |
26 | Source1: coqide.desktop |
27 | Source2: coqide.xpm | |
672cbc20 | 28 | Patch0: %{name}-dune-prefix.patch |
10fd38a7 | 29 | URL: https://coq.inria.fr/ |
5f0acdc3 | 30 | BuildRequires: bash |
b2cb8983 | 31 | BuildRequires: ocaml >= 1:4.05 |
5f0acdc3 | 32 | BuildRequires: camlp5 >= 5.01 |
672cbc20 | 33 | BuildRequires: ocaml-dune >= 2.5.0 |
b2cb8983 JR |
34 | BuildRequires: ocaml-findlib >= 1.8.1 |
35 | BuildRequires: ocaml-zarith-devel >= 1.10 | |
10fd38a7 JB |
36 | BuildRequires: ocaml-lablgtk3-devel >= 3.1.0 |
37 | BuildRequires: ocaml-lablgtk3-gtksourceview-devel >= 3.1.0 | |
5f0acdc3 | 38 | BuildRequires: sed >= 4.0 |
10fd38a7 JB |
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) | |
9e2234f9 | 50 | BuildRequires: texlive-fonts-cmextra |
83437006 | 51 | BuildRequires: texlive-fonts-cmsuper |
9e2234f9 | 52 | BuildRequires: texlive-fonts-other |
83437006 | 53 | BuildRequires: texlive-format-pdflatex |
308e7511 | 54 | BuildRequires: texlive-latex-ams |
8bee228d | 55 | BuildRequires: texlive-latex-comment |
b46eabb1 | 56 | BuildRequires: texlive-latex-moreverb |
83437006 JB |
57 | BuildRequires: texlive-latex-ucs |
58 | BuildRequires: texlive-makeindex | |
8edb6738 | 59 | BuildRequires: texlive-psutils |
83437006 JB |
60 | # hyperref.sty (from latex) requires ifxexex.sty (from xetex) |
61 | BuildRequires: texlive-xetex | |
10fd38a7 JB |
62 | %endif |
63 | %if %{with sse2} | |
64 | Requires: cpuinfo(sse2) | |
65 | %endif | |
672cbc20 | 66 | Requires: ocaml-coq-devel = %{version}-%{release} |
b2cb8983 | 67 | Obsoletes: coq-emacs < 8.13.1 |
3e0583a4 | 68 | # same as ocaml-zarith |
39bb0263 | 69 | ExclusiveArch: %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 |
680764bb JR |
70 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) |
71 | ||
3809f5df JR |
72 | # Exclude private ocaml interfaces |
73 | %define _noautoreq ocamlx?\\\((Configwin_types|Interface|Richpp|Serialize|Xml_p(arser|rinter)|Xmlprotocol)\\\) | |
74 | ||
680764bb JR |
75 | %description |
76 | Coq is a proof assistant which: | |
bcd66107 | 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. | |
3432574d | 82 | |
3f4e388b JR |
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, | |
b2cb8983 JR |
89 | - wyciągać program o dowiedzionej poprawności z konstruktywnego dowodu |
90 | jego formalnej specyfikacji. | |
9019ffc7 | 91 | |
672cbc20 JB |
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 | ||
9019ffc7 | 117 | %package latex |
10fd38a7 JB |
118 | Summary: Coq documentation style for LaTeX |
119 | Summary(pl.UTF-8): Styl dokumentacji Coq dla LaTeXa | |
9019ffc7 JR |
120 | Group: Development/Tools |
121 | Requires: %{name} = %{version}-%{release} | |
122 | ||
123 | %description latex | |
10fd38a7 | 124 | Coq documentation style for LaTeX. |
9019ffc7 JR |
125 | |
126 | %description latex -l pl.UTF-8 | |
10fd38a7 | 127 | Styl dokumentacji Coq dla LaTeXa. |
9019ffc7 | 128 | |
680764bb JR |
129 | %prep |
130 | %setup -q | |
672cbc20 | 131 | %patch0 -p1 |
5f0acdc3 | 132 | |
672cbc20 | 133 | %{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' tools/configure/configure.ml |
e041a8de JB |
134 | %if %{without sse2} |
135 | %{__sed} -i -e '/cflags_sse2/ s/-msse2 -mfpmath=sse//' tools/configure/configure.ml | |
10fd38a7 | 136 | %endif |
672cbc20 | 137 | %{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in |
b2cb8983 | 138 | |
672cbc20 | 139 | %{__sed} -i -e '1s,/usr/bin/env python3,%{__python3},' \ |
b2cb8983 JR |
140 | tools/make-both-single-timing-files.py \ |
141 | tools/make-both-time-files.py \ | |
142 | tools/make-one-time-file.py | |
143 | ||
672cbc20 | 144 | %{__sed} -i -e '1s,/usr/bin/env python2,%{__python3},' \ |
b2cb8983 | 145 | doc/tools/coqrst/notations/fontsupport.py |
680764bb JR |
146 | |
147 | %build | |
148 | ./configure \ | |
672cbc20 | 149 | -prefix %{_prefix} \ |
650aa0b6 | 150 | -configdir %{_sysconfdir}/%{name} \ |
10fd38a7 JB |
151 | -datadir %{_datadir}/%{name} \ |
152 | -docdir %{_docdir}/%{name}-%{version} \ | |
153 | -libdir %{_libdir}/coq \ | |
154 | -mandir %{_mandir} \ | |
b2cb8983 | 155 | %if %{with ocaml_opt} |
b2cb8983 | 156 | -coqide opt \ |
10fd38a7 | 157 | -native-compiler yes \ |
b2cb8983 JR |
158 | %else |
159 | -byte-only \ | |
b2cb8983 | 160 | -coqide byte \ |
10fd38a7 | 161 | -native-compiler no \ |
b2cb8983 | 162 | %endif |
10fd38a7 JB |
163 | -browser "xdg-open %s" \ |
164 | %{?with_doc:-with-doc yes} | |
680764bb | 165 | |
672cbc20 JB |
166 | %{__make} world \ |
167 | CAML_LD_LIBRARY_PATH=kernel/byterun \ | |
168 | _DDISPLAY=verbose \ | |
169 | VERBOSE=1 | |
b2cb8983 | 170 | %{?with_tests:%{__make} check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories |
680764bb JR |
171 | |
172 | %install | |
173 | rm -rf $RPM_BUILD_ROOT | |
672cbc20 | 174 | install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir},%{_sysconfdir}/%{name}} |
3432574d | 175 | |
b2cb8983 | 176 | %{__make} install \ |
672cbc20 JB |
177 | _DDISPLAY=verbose \ |
178 | DESTDIR=$RPM_BUILD_ROOT | |
680764bb | 179 | |
b2cb8983 JR |
180 | cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} |
181 | cp -p %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} | |
8bee228d | 182 | |
672cbc20 JB |
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 | |
c10c241b | 191 | |
680764bb JR |
192 | %clean |
193 | rm -rf $RPM_BUILD_ROOT | |
194 | ||
195 | %files | |
196 | %defattr(644,root,root,755) | |
c10c241b | 197 | %doc %{_docdir}/%{name}-%{version} |
650aa0b6 | 198 | %dir %{_sysconfdir}/%{name} |
672cbc20 JB |
199 | %attr(755,root,root) %{_bindir}/coq-tex |
200 | %attr(755,root,root) %{_bindir}/coq_makefile | |
680764bb | 201 | %attr(755,root,root) %{_bindir}/coqc |
672cbc20 | 202 | %attr(755,root,root) %{_bindir}/coqc.byte |
2dc46485 | 203 | %attr(755,root,root) %{_bindir}/coqchk |
680764bb | 204 | %attr(755,root,root) %{_bindir}/coqdep |
1c74cbbc | 205 | %attr(755,root,root) %{_bindir}/coqdoc |
672cbc20 JB |
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 | |
b2cb8983 JR |
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 | |
861daf7b | 214 | %attr(755,root,root) %{_bindir}/coqtop |
672cbc20 | 215 | %attr(755,root,root) %{_bindir}/coqtop.byte |
b2cb8983 | 216 | %attr(755,root,root) %{_bindir}/coqtop.opt |
1c74cbbc | 217 | %attr(755,root,root) %{_bindir}/coqwc |
6b871b2b | 218 | %attr(755,root,root) %{_bindir}/coqworkmgr |
672cbc20 | 219 | %attr(755,root,root) %{_bindir}/csdpcert |
b2cb8983 JR |
220 | %attr(755,root,root) %{_bindir}/ocamllibdep |
221 | %attr(755,root,root) %{_bindir}/votour | |
3432574d | 222 | %dir %{_libdir}/coq |
672cbc20 JB |
223 | %{_libdir}/coq/theories |
224 | %{_libdir}/coq/user-contrib | |
9019ffc7 JR |
225 | %{_mandir}/man1/coq_makefile.1* |
226 | %{_mandir}/man1/coq-tex.1* | |
680764bb | 227 | %{_mandir}/man1/coqc.1* |
2dc46485 JR |
228 | %{_mandir}/man1/coqchk.1* |
229 | %{_mandir}/man1/coqdep.1* | |
230 | %{_mandir}/man1/coqdoc.1* | |
2dc46485 | 231 | %{_mandir}/man1/coqide.1* |
672cbc20 | 232 | %{_mandir}/man1/coqnative.1* |
680764bb JR |
233 | %{_mandir}/man1/coqtop.1* |
234 | %{_mandir}/man1/coqtop.byte.1* | |
9e2234f9 | 235 | %{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*} |
1c74cbbc | 236 | %{_mandir}/man1/coqwc.1* |
8bee228d JR |
237 | %{_desktopdir}/coqide.desktop |
238 | %{_pixmapsdir}/coqide.xpm | |
650aa0b6 | 239 | %{_datadir}/%{name} |
9019ffc7 | 240 | |
672cbc20 JB |
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 | ||
9019ffc7 JR |
696 | %files latex |
697 | %defattr(644,root,root,755) | |
698 | %{_datadir}/texmf/tex/latex/misc/coqdoc.sty |