[packages/coq] - updated to 8.15.0 - added dune-prefix patch (install ocaml modules in standard ocaml dir, not dire

qboosh qboosh at pld-linux.org
Sat Jan 29 15:48:40 CET 2022 

commit 672cbc20ebffc4f61631aee96158d814bbeb829b
Author: Jakub Bogusz <qboosh at pld-linux.org>
Date:   Sat Jan 29 15:49:51 2022 +0100

    - updated to 8.15.0
    - added dune-prefix patch (install ocaml modules in standard ocaml dir, not directly in /usr/lib*)
    - package ocaml modules in standard ocaml-coq* packages

 coq-dune-prefix.patch |  42 ++++
 coq.spec              | 546 +++++++++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 562 insertions(+), 26 deletions(-)
---
diff --git a/coq.spec b/coq.spec
index f8073b5..06f6fe9 100644
--- a/coq.spec
+++ b/coq.spec
@@ -16,19 +16,21 @@
 Summary:	The Coq Proof Assistant
 Summary(pl.UTF-8):	Coq - narzędzie pomagające w udowadnianiu
 Name:		coq
-Version:	8.13.1
-Release:	5
+Version:	8.15.0
+Release:	1
 License:	LGPL v2.1
 Group:		Applications/Math
+#Source0Download: https://github.com/coq/coq/releases
 Source0:	https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz
-# Source0-md5:	03ebbf1034c224a0a3327db2d5688c29
+# Source0-md5:	cfa91d270e013b0ebe49120c2101d010
 Source1:	coqide.desktop
 Source2:	coqide.xpm
+Patch0:		%{name}-dune-prefix.patch
 URL:		https://coq.inria.fr/
 BuildRequires:	bash
 BuildRequires:	ocaml >= 1:4.05
 BuildRequires:	camlp5 >= 5.01
-BuildRequires:	ocaml-dune > 2.5.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
@@ -61,7 +63,7 @@ BuildRequires:	texlive-xetex
 %if %{with sse2}
 Requires:	cpuinfo(sse2)
 %endif
-%requires_eq	ocaml-runtime
+Requires:	ocaml-coq-devel = %{version}-%{release}
 Obsoletes:	coq-emacs < 8.13.1
 # same as ocaml-zarith
 ExclusiveArch:	%{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
@@ -87,6 +89,31 @@ Coq to narzędzie pomagające w udowadnianiu, które:
 - wyciągać program o dowiedzionej poprawności z konstruktywnego dowodu
   jego formalnej specyfikacji.
 
+%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.
+
+%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 -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
@@ -101,28 +128,26 @@ Styl dokumentacji Coq dla LaTeXa.
 
 %prep
 %setup -q
+%patch0 -p1
 
-%{__sed} -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.install
-%{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' configure.ml
+%{__sed} -i 's|-Wall.*-O2|%{rpmcflags} -Wno-unused|' tools/configure/configure.ml
 %if %{with sse2}
 %{__sed} -i -e '/cflags_sse2/ s/-msse2 -mfpmath=sse//' configure.ml
 %endif
-%{__sed} -i "s|-oc|-ccopt '%{rpmldflags}' -g &|" Makefile.build
-%{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in Makefile.build
+%{__sed} -i 's,-shared,& -g,g' tools/CoqMakefile.in
 
-%{__sed} -E -i -e '1s,#!\s*/usr/bin/env\s+python3(\s|$),#!%{__python3}\1,' \
+%{__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} -E -i -e '1s,#!\s*/usr/bin/env\s+python2(\s|$),#!%{__python3}\1,' \
+%{__sed} -i -e '1s,/usr/bin/env python2,%{__python3},' \
       doc/tools/coqrst/notations/fontsupport.py
 
 %build
 ./configure \
-	-bindir %{_bindir} \
+	-prefix %{_prefix} \
 	-configdir %{_sysconfdir}/%{name} \
-	-coqdocdir %{_datadir}/texmf/tex/latex/misc \
 	-datadir %{_datadir}/%{name} \
 	-docdir %{_docdir}/%{name}-%{version} \
 	-libdir %{_libdir}/coq \
@@ -138,25 +163,31 @@ Styl dokumentacji Coq dla LaTeXa.
 	-browser "xdg-open %s" \
 	%{?with_doc:-with-doc yes}
 
-%{__make} world VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun
+%{__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} install \
-	COQINSTALLPREFIX=$RPM_BUILD_ROOT%{_prefix} \
-	COQINSTALLPREFIX2=$RPM_BUILD_ROOT%{_sysconfdir} \
-	OLDROOT=%{_prefix} \
-	OLDROOT2=%{_sysconfdir}
-
-# To install only locally the binaries compiled with absolute paths
+	_DDISPLAY=verbose \
+	DESTDIR=$RPM_BUILD_ROOT
 
 cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir}
 cp -p %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir}
 
-cp -p CONTRIBUTING.md CREDITS README.md $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
@@ -165,25 +196,32 @@ rm -rf $RPM_BUILD_ROOT
 %defattr(644,root,root,755)
 %doc %{_docdir}/%{name}-%{version}
 %dir %{_sysconfdir}/%{name}
+%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
 %attr(755,root,root) %{_bindir}/coqdep
 %attr(755,root,root) %{_bindir}/coqdoc
-%attr(755,root,root) %{_bindir}/coqide*
-%attr(755,root,root) %{_bindir}/coq_makefile
+%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}/coq-tex
 %attr(755,root,root) %{_bindir}/coqtop
+%attr(755,root,root) %{_bindir}/coqtop.byte
 %attr(755,root,root) %{_bindir}/coqtop.opt
 %attr(755,root,root) %{_bindir}/coqwc
 %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*
@@ -191,6 +229,7 @@ rm -rf $RPM_BUILD_ROOT
 %{_mandir}/man1/coqdep.1*
 %{_mandir}/man1/coqdoc.1*
 %{_mandir}/man1/coqide.1*
+%{_mandir}/man1/coqnative.1*
 %{_mandir}/man1/coqtop.1*
 %{_mandir}/man1/coqtop.byte.1*
 %{?with_ocaml_opt:%{_mandir}/man1/coqtop.opt.1*}
@@ -199,6 +238,461 @@ rm -rf $RPM_BUILD_ROOT
 %{_pixmapsdir}/coqide.xpm
 %{_datadir}/%{name}
 
+%files -n ocaml-coq
+%defattr(644,root,root,755)
+%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)
 %{_datadir}/texmf/tex/latex/misc/coqdoc.sty
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 *)
================================================================

---- gitweb:

http://git.pld-linux.org/gitweb.cgi/packages/coq.git/commitdiff/672cbc20ebffc4f61631aee96158d814bbeb829b

More information about the pld-cvs-commit mailing list