From: Jakub Bogusz Date: Sat, 29 Jan 2022 16:18:29 +0000 (+0100) Subject: - this version relies on fpmath=sse, so require sse2 on x86 X-Git-Tag: auto/th/coq-8.15.0-1 X-Git-Url: http://git.pld-linux.org/?p=packages%2Fcoq.git;a=commitdiff_plain;h=HEAD;hp=1993b991f3f5a80b24e7144dd64beb40cedf9f90 - this version relies on fpmath=sse, so require sse2 on x86 --- diff --git a/coq-dune-prefix.patch b/coq-dune-prefix.patch new file mode 100644 index 0000000..9bf9dcb --- /dev/null +++ b/coq-dune-prefix.patch @@ -0,0 +1,42 @@ +--- coq-8.15.0/Makefile.install.orig 2022-01-13 12:55:53.000000000 +0100 ++++ coq-8.15.0/Makefile.install 2022-01-28 18:43:46.051635360 +0100 +@@ -55,12 +55,12 @@ endif + # For now, we respect the values given at configure's time. + ifdef DUNE_29_PLUS + install-dune: $(BCONTEXT)/coq-core.install $(BCONTEXT)/coqide-server.install +- dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coq-core +- dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coqide-server ++ dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coq-core ++ dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coqide-server + else + install-dune: $(BCONTEXT)/coq-core.install $(BCONTEXT)/coqide-server.install +- dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" coq-core +- dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" coqide-server ++ dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" coq-core ++ dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" coqide-server + endif + + # IMPORTANT NOTE: before Dune 2.9, the --docdir and --etcdir options +@@ -103,9 +103,9 @@ install-coqide: + else + ifdef DUNE_29_PLUS + install-coqide: $(BCONTEXT)/coqide.install +- dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coqide ++ dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coqide + else +- dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" coqide ++ dune install $(_DOPT) $(DESTDIRARG) --mandir="$(MANDIR)" coqide + endif + endif + +--- coq-8.15.0/boot/env.ml.orig 2022-01-13 12:55:53.000000000 +0100 ++++ coq-8.15.0/boot/env.ml 2022-01-29 08:35:32.771267459 +0100 +@@ -48,7 +48,7 @@ let guess_coqlib () = + let guess_coqcorelib lib = + if Sys.file_exists (Path.relative lib "plugins") + then lib +- else Path.relative lib "../coq-core" ++ else Path.relative lib "../ocaml/coq-core" + + (* Should we fail on double initialization? That seems a way to avoid + mis-use for example when we pass command line arguments *) diff --git a/coq-lablgtk2.patch b/coq-lablgtk2.patch deleted file mode 100644 index 1102759..0000000 --- a/coq-lablgtk2.patch +++ /dev/null @@ -1,46 +0,0 @@ ---- coq-8.1pl4/configure~ 2008-10-09 11:40:41.000000000 +0200 -+++ coq-8.1pl4/configure 2009-02-16 14:03:00.496249846 +0100 -@@ -634,7 +634,7 @@ - # Beware of the final \r in Win32 - lablgtkdirtmp="$(ocamlfind query lablgtk2 2> /dev/null | tr -d '\r')" - if [ "$lablgtkdirtmp" != "" ]; then -- if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then -+ if [ -f "$lablgtkdirtmp/glib.cmi" -o -f "$lablgtkdirtmp/glib.mli" ]; then - lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind" - lablgtkdir=$lablgtkdirtmp - LABLGTKLIB=$lablgtkdir # Pour le message utilisateur -@@ -652,7 +652,7 @@ - echo "$lablgtkdir is not a valid directory." - echo "Configuration script failed!" - exit 1 -- elif [ -f "$lablgtkdir/glib.cmi" -a -f "$lablgtkdir/glib.mli" ]; then -+ elif [ -f "$lablgtkdir/glib.cmi" -o -f "$lablgtkdir/glib.mli" ]; then - lablgtkdirfoundmsg="LablGtk2 directory found" - LABLGTKLIB=$lablgtkdir # Pour le message utilisateur - else -@@ -664,9 +664,6 @@ - if [ "$lablgtkdir" = "" ]; then - echo "LablGtk2 not found: CoqIde will not be available." - COQIDE=no -- elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then -- echo "$lablgtkdirfoundmsg but too old: CoqIde will not be available." -- COQIDE=no; - elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then - echo "$lablgtkdirfoundmsg, bytecode CoqIde will be used as requested." - COQIDE=byte -@@ -855,15 +852,7 @@ - #################################################### - - if [ ! "$COQIDE" = "no" ]; then -- if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then -- if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then - cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli -- else -- cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli -- fi -- else -- cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli -- fi - fi - - ################################################## diff --git a/coq.spec b/coq.spec index a8b512a..a7e34f3 100644 --- a/coq.spec +++ b/coq.spec @@ -1,36 +1,52 @@ # -# TODO: -# - package and R: Csdp (https://projects.coin-or.org/Csdp) -# # Conditional build: -%bcond_without ocaml_opt # skip building native optimized binaries (bytecode is always built) +%bcond_without ocaml_opt # native optimized binaries (bytecode is always built) +%bcond_without sse2 # SSE2 instructions (i387 maths not supported as of 8.15) +%bcond_with doc # documentation %bcond_with tests # run testsuite (csdp dependant micromega tests fail badly on x86_64) # -%ifnarch %{ix86} %{x8664} arm aarch64 ppc sparc sparcv9 +%ifarch pentium4 %{x8664} x32 +%define with_sse2 1 +%endif + +%ifnarch %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 %undefine with_ocaml_opt %endif Summary: The Coq Proof Assistant Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu Name: coq -Version: 8.4pl6 -Release: 3 +Version: 8.15.0 +Release: 1 License: LGPL v2.1 Group: Applications/Math -Source0: http://coq.inria.fr/distrib/V%{version}/files/%{name}-%{version}.tar.gz -# Source0-md5: 2334a98b64578cb81d2b4127e327b368 +#Source0Download: https://github.com/coq/coq/releases +Source0: https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz +# Source0-md5: cfa91d270e013b0ebe49120c2101d010 Source1: coqide.desktop Source2: coqide.xpm -Patch0: %{name}-lablgtk2.patch -URL: http://coq.inria.fr/ +Patch0: %{name}-dune-prefix.patch +URL: https://coq.inria.fr/ BuildRequires: bash -BuildRequires: emacs -BuildRequires: hevea -BuildRequires: netpbm-progs -BuildRequires: ocaml >= 3.09.0 +BuildRequires: ocaml >= 1:4.05 BuildRequires: camlp5 >= 5.01 -BuildRequires: ocaml-lablgtk2-devel >= 2.12.0 +BuildRequires: ocaml-dune >= 2.5.0 +BuildRequires: ocaml-findlib >= 1.8.1 +BuildRequires: ocaml-zarith-devel >= 1.10 +BuildRequires: ocaml-lablgtk3-devel >= 3.1.0 +BuildRequires: ocaml-lablgtk3-gtksourceview-devel >= 3.1.0 BuildRequires: sed >= 4.0 +%if %{with doc} +BuildRequires: python3 >= 1:3 +# TODO (and adjust package name) +BuildRequires: python3-antlr4-python3-runtime >= 4.7.1 +BuildRequires: python3-bs4 >= 4.0.6 +BuildRequires: python3-pexpect >= 4.2.1 +BuildRequires: python3-sphinx_rtd_theme >= 0.4.3 +# TODO (and adjust package name) +BuildRequires: python3-sphinxcontrib-bibtex >= 0.4.2 +BuildRequires: sphinx-pdg >= 2.3.1 +# TODO: update texlive packages list (or drop pdf building leaving only html) BuildRequires: texlive-fonts-cmextra BuildRequires: texlive-fonts-cmsuper BuildRequires: texlive-fonts-other @@ -43,9 +59,19 @@ BuildRequires: texlive-makeindex BuildRequires: texlive-psutils # hyperref.sty (from latex) requires ifxexex.sty (from xetex) BuildRequires: texlive-xetex -%requires_eq ocaml-runtime +%endif +%if %{with sse2} +Requires: cpuinfo(sse2) +%endif +Requires: ocaml-coq-devel = %{version}-%{release} +Obsoletes: coq-emacs < 8.13.1 +# same as ocaml-zarith +ExclusiveArch: %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) +# Exclude private ocaml interfaces +%define _noautoreq ocamlx?\\\((Configwin_types|Interface|Richpp|Serialize|Xml_p(arser|rinter)|Xmlprotocol)\\\) + %description Coq is a proof assistant which: - allows to handle calculus assertions, @@ -60,72 +86,108 @@ Coq to narzędzie pomagające w udowadnianiu, które: różniczkowego, - mechanicznie sprawdzać dowody tych twierdzeń, - pomagać w znalezieniu formalnych dowodów, -- wyciągać program o dowiedzionej poprawności z konstruktywnego - dowodu jego formalnej specyfikacji. +- wyciągać program o dowiedzionej poprawności z konstruktywnego dowodu + jego formalnej specyfikacji. -%package emacs -Summary: Emacs mode and syntax for Coq -Summary(pl.UTF-8): Tryb i składnia Coq dla Emacsa -Group: Development/Tools -Requires: %{name} = %{version}-%{release} +%package -n ocaml-coq +Summary: Coq Proof Assistant - OCaml runtime libraries +Summary(pl.UTF-8): Asystent udowadniania Coq - biblioteki uruchomieniowe OCamla +Group: Libraries +%requires_eq ocaml-runtime + +%description -n ocaml-coq +Coq Proof Assistant - OCaml runtime libraries. + +%description -n ocaml-coq -l pl.UTF-8 +Asystent udowadniania Coq - biblioteki uruchomieniowe OCamla. -%description emacs -Emacs mode and suyntax files for Coq. +%package -n ocaml-coq-devel +Summary: Coq Proof Assistant - OCaml development libraries +Summary(pl.UTF-8): Asystent udowadniania Coq - biblioteki programistyczne OCamla +Group: Development/Libraries +Requires: ocaml-coq = %{version}-%{release} +%requires_eq ocaml -%description emacs -l pl.UTF-8 -Pliki trybu i składni Coq dla Emacsa. +%description -n ocaml-coq-devel +Coq Proof Assistant - OCaml development libraries. + +%description -n ocaml-coq-devel -l pl.UTF-8 +Asystent udowadniania Coq - biblioteki programistyczne OCamla. %package latex -Summary: Coq documentation style for latex -Summary(pl.UTF-8): Styl dokumentacji Coq dla latexa +Summary: Coq documentation style for LaTeX +Summary(pl.UTF-8): Styl dokumentacji Coq dla LaTeXa Group: Development/Tools Requires: %{name} = %{version}-%{release} %description latex -Coq documentation style for latex. +Coq documentation style for LaTeX. %description latex -l pl.UTF-8 -Styl dokumentacji Coq dla latexa. +Styl dokumentacji Coq dla LaTeXa. %prep %setup -q %patch0 -p1 -%{__sed} -i -e 's|#!/bin/sh|#!/bin/bash|' test-suite/check -%{__sed} -i -e 's|\(MAKE_TSOPTS=.*\) -s \(.*\)|\1 \2|' Makefile.build +%{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' tools/configure/configure.ml +%if %{without sse2} +%{__sed} -i -e '/cflags_sse2/ s/-msse2 -mfpmath=sse//' tools/configure/configure.ml +%endif +%{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in + +%{__sed} -i -e '1s,/usr/bin/env python3,%{__python3},' \ + tools/make-both-single-timing-files.py \ + tools/make-both-time-files.py \ + tools/make-one-time-file.py + +%{__sed} -i -e '1s,/usr/bin/env python2,%{__python3},' \ + doc/tools/coqrst/notations/fontsupport.py %build ./configure \ - -bindir %{_bindir} \ - -libdir %{_libdir}/coq \ - -mandir %{_mandir} \ - -docdir %{_docdir}/%{name}-%{version} \ + -prefix %{_prefix} \ -configdir %{_sysconfdir}/%{name} \ -datadir %{_datadir}/%{name} \ - -emacs emacs \ + -docdir %{_docdir}/%{name}-%{version} \ + -libdir %{_libdir}/coq \ + -mandir %{_mandir} \ +%if %{with ocaml_opt} + -coqide opt \ + -native-compiler yes \ +%else + -byte-only \ + -coqide byte \ + -native-compiler no \ +%endif -browser "xdg-open %s" \ - -emacslib %{_datadir}/emacs/site-lisp \ - %{?with_ocaml_opt:-opt} \ - --coqdocdir %{_datadir}/texmf/tex/latex/misc \ - --coqide %{?with_ocaml_opt:opt}%{!?with_ocaml_opt:byte} + %{?with_doc:-with-doc yes} -%{__make} -j1 world VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun -%{?with_tests:%{__make} -j1 check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories +%{__make} world \ + CAML_LD_LIBRARY_PATH=kernel/byterun \ + _DDISPLAY=verbose \ + VERBOSE=1 +%{?with_tests:%{__make} check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories %install rm -rf $RPM_BUILD_ROOT -install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}} +install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir},%{_sysconfdir}/%{name}} -%{__make} -e install \ - COQINSTALLPREFIX=$RPM_BUILD_ROOT/ -# To install only locally the binaries compiled with absolute paths +%{__make} install \ + _DDISPLAY=verbose \ + DESTDIR=$RPM_BUILD_ROOT -install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} -install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} +cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} +cp -p %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} -# pdf is enough -%{__rm} -r $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}/ps -cp -p CHANGES COMPATIBILITY COPYRIGHT CREDITS README $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version} +cp -p CREDITS README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version} + +%{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*.ml +%{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*/*.ml +%{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/*/*/*/*.ml +%{__rm} $RPM_BUILD_ROOT%{_libdir}/ocaml/coqide-server/*/*.ml +# build time +%{__rm} -r $RPM_BUILD_ROOT%{_libdir}/ocaml/coq-core/tools %clean rm -rf $RPM_BUILD_ROOT @@ -134,23 +196,32 @@ rm -rf $RPM_BUILD_ROOT %defattr(644,root,root,755) %doc %{_docdir}/%{name}-%{version} %dir %{_sysconfdir}/%{name} -%config(noreplace) %verify(not md5 mtime size) %{_sysconfdir}/%{name}/coqide-gtk2rc -%attr(755,root,root) %{_bindir}/coq_makefile %attr(755,root,root) %{_bindir}/coq-tex +%attr(755,root,root) %{_bindir}/coq_makefile %attr(755,root,root) %{_bindir}/coqc +%attr(755,root,root) %{_bindir}/coqc.byte %attr(755,root,root) %{_bindir}/coqchk -%{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqchk.opt} %attr(755,root,root) %{_bindir}/coqdep %attr(755,root,root) %{_bindir}/coqdoc -%attr(755,root,root) %{_bindir}/coqide* -%attr(755,root,root) %{_bindir}/coqmktop +%attr(755,root,root) %{_bindir}/coqide +%attr(755,root,root) %{_bindir}/coqidetop.byte +%attr(755,root,root) %{_bindir}/coqidetop.opt +%attr(755,root,root) %{_bindir}/coqnative +%attr(755,root,root) %{_bindir}/coqpp +%attr(755,root,root) %{_bindir}/coqproofworker.opt +%attr(755,root,root) %{_bindir}/coqqueryworker.opt +%attr(755,root,root) %{_bindir}/coqtacticworker.opt %attr(755,root,root) %{_bindir}/coqtop %attr(755,root,root) %{_bindir}/coqtop.byte -%{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqtop.opt} +%attr(755,root,root) %{_bindir}/coqtop.opt %attr(755,root,root) %{_bindir}/coqwc -%attr(755,root,root) %{_bindir}/gallina +%attr(755,root,root) %{_bindir}/coqworkmgr +%attr(755,root,root) %{_bindir}/csdpcert +%attr(755,root,root) %{_bindir}/ocamllibdep +%attr(755,root,root) %{_bindir}/votour %dir %{_libdir}/coq -%{_libdir}/coq/* +%{_libdir}/coq/theories +%{_libdir}/coq/user-contrib %{_mandir}/man1/coq_makefile.1* %{_mandir}/man1/coq-tex.1* %{_mandir}/man1/coqc.1* @@ -158,23 +229,469 @@ rm -rf $RPM_BUILD_ROOT %{_mandir}/man1/coqdep.1* %{_mandir}/man1/coqdoc.1* %{_mandir}/man1/coqide.1* -%{_mandir}/man1/coqmktop.1* +%{_mandir}/man1/coqnative.1* %{_mandir}/man1/coqtop.1* %{_mandir}/man1/coqtop.byte.1* %{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*} %{_mandir}/man1/coqwc.1* -%{_mandir}/man1/gallina.1* %{_desktopdir}/coqide.desktop %{_pixmapsdir}/coqide.xpm %{_datadir}/%{name} -%files emacs +%files -n ocaml-coq %defattr(644,root,root,755) -%{_datadir}/emacs/site-lisp/coq.el -%{_datadir}/emacs/site-lisp/coq-db.el -%{_datadir}/emacs/site-lisp/coq-font-lock.el -%{_datadir}/emacs/site-lisp/coq-inferior.el -%{_datadir}/emacs/site-lisp/coq-syntax.el +%dir %{_libdir}/ocaml/coq-core +%{_libdir}/ocaml/coq-core/META +%{_libdir}/ocaml/coq-core/revision +%dir %{_libdir}/ocaml/coq-core/boot +%{_libdir}/ocaml/coq-core/boot/*.cma +%dir %{_libdir}/ocaml/coq-core/clib +%{_libdir}/ocaml/coq-core/clib/*.cma +%dir %{_libdir}/ocaml/coq-core/config +%{_libdir}/ocaml/coq-core/config/*.cma +%dir %{_libdir}/ocaml/coq-core/engine +%{_libdir}/ocaml/coq-core/engine/*.cma +%dir %{_libdir}/ocaml/coq-core/gramlib +%{_libdir}/ocaml/coq-core/gramlib/*.cma +%dir %{_libdir}/ocaml/coq-core/interp +%{_libdir}/ocaml/coq-core/interp/*.cma +%dir %{_libdir}/ocaml/coq-core/kernel +%{_libdir}/ocaml/coq-core/kernel/*.cma +%dir %{_libdir}/ocaml/coq-core/lib +%{_libdir}/ocaml/coq-core/lib/*.cma +%dir %{_libdir}/ocaml/coq-core/library +%{_libdir}/ocaml/coq-core/library/*.cma +%dir %{_libdir}/ocaml/coq-core/parsing +%{_libdir}/ocaml/coq-core/parsing/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins +%dir %{_libdir}/ocaml/coq-core/plugins/btauto +%{_libdir}/ocaml/coq-core/plugins/btauto/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/cc +%{_libdir}/ocaml/coq-core/plugins/cc/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/derive +%{_libdir}/ocaml/coq-core/plugins/derive/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/extraction +%{_libdir}/ocaml/coq-core/plugins/extraction/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/firstorder +%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/funind +%{_libdir}/ocaml/coq-core/plugins/funind/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/ltac +%{_libdir}/ocaml/coq-core/plugins/ltac/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/ltac2 +%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/micromega +%{_libdir}/ocaml/coq-core/plugins/micromega/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/nsatz +%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/number_string_notation +%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/ring +%{_libdir}/ocaml/coq-core/plugins/ring/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/rtauto +%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/ssreflect +%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/ssrmatching +%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/tauto +%{_libdir}/ocaml/coq-core/plugins/tauto/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/tutorial +%dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p0 +%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p1 +%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p2 +%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/tutorial/p3 +%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cma +%dir %{_libdir}/ocaml/coq-core/plugins/zify +%{_libdir}/ocaml/coq-core/plugins/zify/*.cma +%dir %{_libdir}/ocaml/coq-core/pretyping +%{_libdir}/ocaml/coq-core/pretyping/*.cma +%dir %{_libdir}/ocaml/coq-core/printing +%{_libdir}/ocaml/coq-core/printing/*.cma +%dir %{_libdir}/ocaml/coq-core/proofs +%{_libdir}/ocaml/coq-core/proofs/*.cma +%dir %{_libdir}/ocaml/coq-core/stm +%{_libdir}/ocaml/coq-core/stm/*.cma +%dir %{_libdir}/ocaml/coq-core/sysinit +%{_libdir}/ocaml/coq-core/sysinit/*.cma +%dir %{_libdir}/ocaml/coq-core/tactics +%{_libdir}/ocaml/coq-core/tactics/*.cma +%dir %{_libdir}/ocaml/coq-core/top_printers +%{_libdir}/ocaml/coq-core/top_printers/*.cma +%dir %{_libdir}/ocaml/coq-core/toplevel +%{_libdir}/ocaml/coq-core/toplevel/*.cma +%dir %{_libdir}/ocaml/coq-core/vernac +%{_libdir}/ocaml/coq-core/vernac/*.cma +%dir %{_libdir}/ocaml/coq-core/vm +%{_libdir}/ocaml/coq-core/vm/*.cma +%dir %{_libdir}/ocaml/coqide +%{_libdir}/ocaml/coqide/META +%dir %{_libdir}/ocaml/coqide-server +%{_libdir}/ocaml/coqide-server/META +%dir %{_libdir}/ocaml/coqide-server/core +%{_libdir}/ocaml/coqide-server/core/*.cma +%dir %{_libdir}/ocaml/coqide-server/protocol +%{_libdir}/ocaml/coqide-server/protocol/*.cma +%if %{with ocaml_opt} +%attr(755,root,root) %{_libdir}/ocaml/coq-core/boot/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/clib/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/config/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/engine/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/gramlib/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/interp/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/kernel/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/lib/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/library/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/parsing/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/btauto/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/cc/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/derive/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/extraction/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/funind/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ltac/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/micromega/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ring/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tauto/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/plugins/zify/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/pretyping/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/printing/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/proofs/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/stm/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/sysinit/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/tactics/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/top_printers/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/toplevel/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/vernac/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coq-core/vm/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coqide-server/core/*.cmxs +%attr(755,root,root) %{_libdir}/ocaml/coqide-server/protocol/*.cmxs +%endif +%attr(755,root,root) %{_libdir}/ocaml/stublibs/dllcoqrun_stubs.so + +%files -n ocaml-coq-devel +%defattr(644,root,root,755) +%{_libdir}/ocaml/coq-core/dune-package +%{_libdir}/ocaml/coq-core/opam +%{_libdir}/ocaml/coq-core/boot/*.cmi +%{_libdir}/ocaml/coq-core/boot/*.cmt +%{_libdir}/ocaml/coq-core/boot/*.cmti +%{_libdir}/ocaml/coq-core/boot/*.mli +%{_libdir}/ocaml/coq-core/clib/*.cmi +%{_libdir}/ocaml/coq-core/clib/*.cmt +%{_libdir}/ocaml/coq-core/clib/*.cmti +%{_libdir}/ocaml/coq-core/clib/*.mli +%{_libdir}/ocaml/coq-core/config/*.cmi +%{_libdir}/ocaml/coq-core/config/*.cmt +%{_libdir}/ocaml/coq-core/config/*.cmti +%{_libdir}/ocaml/coq-core/config/*.mli +%{_libdir}/ocaml/coq-core/engine/*.cmi +%{_libdir}/ocaml/coq-core/engine/*.cmt +%{_libdir}/ocaml/coq-core/engine/*.cmti +%{_libdir}/ocaml/coq-core/engine/*.mli +%{_libdir}/ocaml/coq-core/gramlib/*.cmi +%{_libdir}/ocaml/coq-core/gramlib/*.cmt +%{_libdir}/ocaml/coq-core/gramlib/*.cmti +%{_libdir}/ocaml/coq-core/gramlib/*.mli +%{_libdir}/ocaml/coq-core/interp/*.cmi +%{_libdir}/ocaml/coq-core/interp/*.cmt +%{_libdir}/ocaml/coq-core/interp/*.cmti +%{_libdir}/ocaml/coq-core/interp/*.mli +%{_libdir}/ocaml/coq-core/kernel/*.cmi +%{_libdir}/ocaml/coq-core/kernel/*.cmt +%{_libdir}/ocaml/coq-core/kernel/*.cmti +%{_libdir}/ocaml/coq-core/kernel/*.mli +%{_libdir}/ocaml/coq-core/lib/*.cmi +%{_libdir}/ocaml/coq-core/lib/*.cmt +%{_libdir}/ocaml/coq-core/lib/*.cmti +%{_libdir}/ocaml/coq-core/lib/*.mli +%{_libdir}/ocaml/coq-core/library/*.cmi +%{_libdir}/ocaml/coq-core/library/*.cmt +%{_libdir}/ocaml/coq-core/library/*.cmti +%{_libdir}/ocaml/coq-core/library/*.mli +%{_libdir}/ocaml/coq-core/parsing/*.cmi +%{_libdir}/ocaml/coq-core/parsing/*.cmt +%{_libdir}/ocaml/coq-core/parsing/*.cmti +%{_libdir}/ocaml/coq-core/parsing/*.mli +%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmi +%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmt +%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmti +%{_libdir}/ocaml/coq-core/plugins/btauto/*.mli +%{_libdir}/ocaml/coq-core/plugins/cc/*.cmi +%{_libdir}/ocaml/coq-core/plugins/cc/*.cmt +%{_libdir}/ocaml/coq-core/plugins/cc/*.cmti +%{_libdir}/ocaml/coq-core/plugins/cc/*.mli +%{_libdir}/ocaml/coq-core/plugins/derive/*.cmi +%{_libdir}/ocaml/coq-core/plugins/derive/*.cmt +%{_libdir}/ocaml/coq-core/plugins/derive/*.cmti +%{_libdir}/ocaml/coq-core/plugins/derive/*.mli +%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmi +%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmt +%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmti +%{_libdir}/ocaml/coq-core/plugins/extraction/*.mli +%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmi +%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmt +%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmti +%{_libdir}/ocaml/coq-core/plugins/firstorder/*.mli +%{_libdir}/ocaml/coq-core/plugins/funind/*.cmi +%{_libdir}/ocaml/coq-core/plugins/funind/*.cmt +%{_libdir}/ocaml/coq-core/plugins/funind/*.cmti +%{_libdir}/ocaml/coq-core/plugins/funind/*.mli +%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmi +%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmt +%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmti +%{_libdir}/ocaml/coq-core/plugins/ltac/*.mli +%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmi +%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmt +%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmti +%{_libdir}/ocaml/coq-core/plugins/ltac2/*.mli +%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmi +%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmt +%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmti +%{_libdir}/ocaml/coq-core/plugins/micromega/*.mli +%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmi +%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmt +%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmti +%{_libdir}/ocaml/coq-core/plugins/nsatz/*.mli +%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmi +%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmt +%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmti +%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.mli +%{_libdir}/ocaml/coq-core/plugins/ring/*.cmi +%{_libdir}/ocaml/coq-core/plugins/ring/*.cmt +%{_libdir}/ocaml/coq-core/plugins/ring/*.cmti +%{_libdir}/ocaml/coq-core/plugins/ring/*.mli +%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmi +%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmt +%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmti +%{_libdir}/ocaml/coq-core/plugins/rtauto/*.mli +%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmi +%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmt +%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmti +%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.mli +%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmi +%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmt +%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmti +%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.mli +%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmi +%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmt +%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmti +%{_libdir}/ocaml/coq-core/plugins/tauto/*.mli +%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmi +%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmt +%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmti +%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.mli +%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmi +%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmt +%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmti +%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.mli +%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmi +%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmt +%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmti +%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.mli +%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmi +%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmt +%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmti +%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.mli +%{_libdir}/ocaml/coq-core/plugins/zify/*.cmi +%{_libdir}/ocaml/coq-core/plugins/zify/*.cmt +%{_libdir}/ocaml/coq-core/plugins/zify/*.cmti +%{_libdir}/ocaml/coq-core/plugins/zify/*.mli +%{_libdir}/ocaml/coq-core/pretyping/*.cmi +%{_libdir}/ocaml/coq-core/pretyping/*.cmt +%{_libdir}/ocaml/coq-core/pretyping/*.cmti +%{_libdir}/ocaml/coq-core/pretyping/*.mli +%{_libdir}/ocaml/coq-core/printing/*.cmi +%{_libdir}/ocaml/coq-core/printing/*.cmt +%{_libdir}/ocaml/coq-core/printing/*.cmti +%{_libdir}/ocaml/coq-core/printing/*.mli +%{_libdir}/ocaml/coq-core/proofs/*.cmi +%{_libdir}/ocaml/coq-core/proofs/*.cmt +%{_libdir}/ocaml/coq-core/proofs/*.cmti +%{_libdir}/ocaml/coq-core/proofs/*.mli +%{_libdir}/ocaml/coq-core/stm/*.cmi +%{_libdir}/ocaml/coq-core/stm/*.cmt +%{_libdir}/ocaml/coq-core/stm/*.cmti +%{_libdir}/ocaml/coq-core/stm/*.mli +%{_libdir}/ocaml/coq-core/sysinit/*.cmi +%{_libdir}/ocaml/coq-core/sysinit/*.cmt +%{_libdir}/ocaml/coq-core/sysinit/*.cmti +%{_libdir}/ocaml/coq-core/sysinit/*.mli +%{_libdir}/ocaml/coq-core/tactics/*.cmi +%{_libdir}/ocaml/coq-core/tactics/*.cmt +%{_libdir}/ocaml/coq-core/tactics/*.cmti +%{_libdir}/ocaml/coq-core/tactics/*.mli +%{_libdir}/ocaml/coq-core/top_printers/*.cmi +%{_libdir}/ocaml/coq-core/top_printers/*.cmt +%{_libdir}/ocaml/coq-core/top_printers/*.cmti +%{_libdir}/ocaml/coq-core/top_printers/*.mli +%{_libdir}/ocaml/coq-core/toplevel/*.cmi +%{_libdir}/ocaml/coq-core/toplevel/*.cmt +%{_libdir}/ocaml/coq-core/toplevel/*.cmti +%{_libdir}/ocaml/coq-core/toplevel/*.mli +%{_libdir}/ocaml/coq-core/vernac/*.cmi +%{_libdir}/ocaml/coq-core/vernac/*.cmt +%{_libdir}/ocaml/coq-core/vernac/*.cmti +%{_libdir}/ocaml/coq-core/vernac/*.mli +%{_libdir}/ocaml/coq-core/vm/libcoqrun_stubs.a +%{_libdir}/ocaml/coq-core/vm/*.cmi +%{_libdir}/ocaml/coq-core/vm/*.cmt +%{_libdir}/ocaml/coqide/dune-package +%{_libdir}/ocaml/coqide/opam +%{_libdir}/ocaml/coqide-server/dune-package +%{_libdir}/ocaml/coqide-server/opam +%{_libdir}/ocaml/coqide-server/core/*.cmi +%{_libdir}/ocaml/coqide-server/core/*.cmt +%{_libdir}/ocaml/coqide-server/core/*.cmti +%{_libdir}/ocaml/coqide-server/core/*.mli +%{_libdir}/ocaml/coqide-server/protocol/*.cmi +%{_libdir}/ocaml/coqide-server/protocol/*.cmt +%{_libdir}/ocaml/coqide-server/protocol/*.cmti +%{_libdir}/ocaml/coqide-server/protocol/*.mli +%if %{with ocaml_opt} +%{_libdir}/ocaml/coq-core/boot/boot.a +%{_libdir}/ocaml/coq-core/boot/*.cmx +%{_libdir}/ocaml/coq-core/boot/*.cmxa +%{_libdir}/ocaml/coq-core/clib/clib.a +%{_libdir}/ocaml/coq-core/clib/*.cmx +%{_libdir}/ocaml/coq-core/clib/*.cmxa +%{_libdir}/ocaml/coq-core/config/config.a +%{_libdir}/ocaml/coq-core/config/*.cmx +%{_libdir}/ocaml/coq-core/config/*.cmxa +%{_libdir}/ocaml/coq-core/engine/engine.a +%{_libdir}/ocaml/coq-core/engine/*.cmx +%{_libdir}/ocaml/coq-core/engine/*.cmxa +%{_libdir}/ocaml/coq-core/gramlib/gramlib.a +%{_libdir}/ocaml/coq-core/gramlib/*.cmx +%{_libdir}/ocaml/coq-core/gramlib/*.cmxa +%{_libdir}/ocaml/coq-core/interp/interp.a +%{_libdir}/ocaml/coq-core/interp/*.cmx +%{_libdir}/ocaml/coq-core/interp/*.cmxa +%{_libdir}/ocaml/coq-core/kernel/kernel.a +%{_libdir}/ocaml/coq-core/kernel/*.cmx +%{_libdir}/ocaml/coq-core/kernel/*.cmxa +%{_libdir}/ocaml/coq-core/lib/lib.a +%{_libdir}/ocaml/coq-core/lib/*.cmx +%{_libdir}/ocaml/coq-core/lib/*.cmxa +%{_libdir}/ocaml/coq-core/library/library.a +%{_libdir}/ocaml/coq-core/library/*.cmx +%{_libdir}/ocaml/coq-core/library/*.cmxa +%{_libdir}/ocaml/coq-core/parsing/parsing.a +%{_libdir}/ocaml/coq-core/parsing/*.cmx +%{_libdir}/ocaml/coq-core/parsing/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/btauto/btauto_plugin.a +%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmx +%{_libdir}/ocaml/coq-core/plugins/btauto/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/cc/cc_plugin.a +%{_libdir}/ocaml/coq-core/plugins/cc/*.cmx +%{_libdir}/ocaml/coq-core/plugins/cc/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/derive/derive_plugin.a +%{_libdir}/ocaml/coq-core/plugins/derive/*.cmx +%{_libdir}/ocaml/coq-core/plugins/derive/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/extraction/extraction_plugin.a +%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmx +%{_libdir}/ocaml/coq-core/plugins/extraction/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/firstorder/firstorder_plugin.a +%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmx +%{_libdir}/ocaml/coq-core/plugins/firstorder/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/funind/funind_plugin.a +%{_libdir}/ocaml/coq-core/plugins/funind/*.cmx +%{_libdir}/ocaml/coq-core/plugins/funind/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/ltac/ltac_plugin.a +%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmx +%{_libdir}/ocaml/coq-core/plugins/ltac/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/ltac2/ltac2_plugin.a +%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmx +%{_libdir}/ocaml/coq-core/plugins/ltac2/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/micromega/micromega_plugin.a +%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmx +%{_libdir}/ocaml/coq-core/plugins/micromega/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/nsatz/nsatz_plugin.a +%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmx +%{_libdir}/ocaml/coq-core/plugins/nsatz/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/number_string_notation/number_string_notation_plugin.a +%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmx +%{_libdir}/ocaml/coq-core/plugins/number_string_notation/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/ring/ring_plugin.a +%{_libdir}/ocaml/coq-core/plugins/ring/*.cmx +%{_libdir}/ocaml/coq-core/plugins/ring/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/rtauto/rtauto_plugin.a +%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmx +%{_libdir}/ocaml/coq-core/plugins/rtauto/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/ssreflect/ssreflect_plugin.a +%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmx +%{_libdir}/ocaml/coq-core/plugins/ssreflect/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/ssrmatching/ssrmatching_plugin.a +%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmx +%{_libdir}/ocaml/coq-core/plugins/ssrmatching/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/tauto/tauto_plugin.a +%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmx +%{_libdir}/ocaml/coq-core/plugins/tauto/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/tuto0_plugin.a +%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmx +%{_libdir}/ocaml/coq-core/plugins/tutorial/p0/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/tuto1_plugin.a +%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmx +%{_libdir}/ocaml/coq-core/plugins/tutorial/p1/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/tuto2_plugin.a +%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmx +%{_libdir}/ocaml/coq-core/plugins/tutorial/p2/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/tuto3_plugin.a +%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmx +%{_libdir}/ocaml/coq-core/plugins/tutorial/p3/*.cmxa +%{_libdir}/ocaml/coq-core/plugins/zify/zify_plugin.a +%{_libdir}/ocaml/coq-core/plugins/zify/*.cmx +%{_libdir}/ocaml/coq-core/plugins/zify/*.cmxa +%{_libdir}/ocaml/coq-core/pretyping/pretyping.a +%{_libdir}/ocaml/coq-core/pretyping/*.cmx +%{_libdir}/ocaml/coq-core/pretyping/*.cmxa +%{_libdir}/ocaml/coq-core/printing/printing.a +%{_libdir}/ocaml/coq-core/printing/*.cmx +%{_libdir}/ocaml/coq-core/printing/*.cmxa +%{_libdir}/ocaml/coq-core/proofs/proofs.a +%{_libdir}/ocaml/coq-core/proofs/*.cmx +%{_libdir}/ocaml/coq-core/proofs/*.cmxa +%{_libdir}/ocaml/coq-core/stm/stm.a +%{_libdir}/ocaml/coq-core/stm/*.cmx +%{_libdir}/ocaml/coq-core/stm/*.cmxa +%{_libdir}/ocaml/coq-core/sysinit/sysinit.a +%{_libdir}/ocaml/coq-core/sysinit/*.cmx +%{_libdir}/ocaml/coq-core/sysinit/*.cmxa +%{_libdir}/ocaml/coq-core/tactics/tactics.a +%{_libdir}/ocaml/coq-core/tactics/*.cmx +%{_libdir}/ocaml/coq-core/tactics/*.cmxa +%{_libdir}/ocaml/coq-core/top_printers/top_printers.a +%{_libdir}/ocaml/coq-core/top_printers/*.cmx +%{_libdir}/ocaml/coq-core/top_printers/*.cmxa +%{_libdir}/ocaml/coq-core/toplevel/toplevel.a +%{_libdir}/ocaml/coq-core/toplevel/*.cmx +%{_libdir}/ocaml/coq-core/toplevel/*.cmxa +%{_libdir}/ocaml/coq-core/vernac/vernac.a +%{_libdir}/ocaml/coq-core/vernac/*.cmx +%{_libdir}/ocaml/coq-core/vernac/*.cmxa +%{_libdir}/ocaml/coq-core/vm/coqrun.a +%{_libdir}/ocaml/coq-core/vm/*.cmx +%{_libdir}/ocaml/coq-core/vm/*.cmxa +%{_libdir}/ocaml/coqide-server/core/core.a +%{_libdir}/ocaml/coqide-server/core/*.cmx +%{_libdir}/ocaml/coqide-server/core/*.cmxa +%{_libdir}/ocaml/coqide-server/protocol/protocol.a +%{_libdir}/ocaml/coqide-server/protocol/*.cmx +%{_libdir}/ocaml/coqide-server/protocol/*.cmxa +%endif %files latex %defattr(644,root,root,755)