git: c3734cabb4d0 - main - math/coq: Update to 8.20.1
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Fri, 14 Feb 2025 03:13:55 UTC
The branch main has been updated by wen:
URL: https://cgit.FreeBSD.org/ports/commit/?id=c3734cabb4d0c3b10dd2b4c92fac9884b9c12161
commit c3734cabb4d0c3b10dd2b4c92fac9884b9c12161
Author: Wen Heping <wen@FreeBSD.org>
AuthorDate: 2025-02-14 02:30:50 +0000
Commit: Wen Heping <wen@FreeBSD.org>
CommitDate: 2025-02-14 03:13:28 +0000
math/coq: Update to 8.20.1
PR: 283111
Reported by: wenheping2000@hotmail.com
Approved by: maintainer(timeout, > 60 days)
---
math/coq/Makefile | 5 +-
math/coq/distinfo | 6 +-
math/coq/pkg-plist | 491 +++++++++++++++++++++++++++++++++++++----------------
3 files changed, 348 insertions(+), 154 deletions(-)
diff --git a/math/coq/Makefile b/math/coq/Makefile
index 0046891ef9a7..f23f57e52b53 100644
--- a/math/coq/Makefile
+++ b/math/coq/Makefile
@@ -1,10 +1,9 @@
PORTNAME= coq
-PORTVERSION= 8.19
-PORTREVISION= 4
+PORTVERSION= 8.20.1
PORTEPOCH= 3
CATEGORIES= math
DISTVERSIONPREFIX= V
-DISTVERSIONSUFFIX= .0
+#DISTVERSIONSUFFIX= .0
PKGNAMESUFFIX= ${EMACS_PKGNAMESUFFIX}
MAINTAINER= hrs@FreeBSD.org
diff --git a/math/coq/distinfo b/math/coq/distinfo
index 8eb59b22d36a..7545f2e3d298 100644
--- a/math/coq/distinfo
+++ b/math/coq/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1707224242
-SHA256 (coq-coq-V8.19.0_GH0.tar.gz) = 17e5c10fadcd3cda7509d822099a892fcd003485272b56a45abd30390f6a426f
-SIZE (coq-coq-V8.19.0_GH0.tar.gz) = 7674352
+TIMESTAMP = 1739496231
+SHA256 (coq-coq-V8.20.1_GH0.tar.gz) = 09ad238cc7930d59564b032be2a8a1fd10d6ef845364d739072d04090a6d3cc2
+SIZE (coq-coq-V8.20.1_GH0.tar.gz) = 7842928
diff --git a/math/coq/pkg-plist b/math/coq/pkg-plist
index a397868e280b..e8d9acdd865d 100644
--- a/math/coq/pkg-plist
+++ b/math/coq/pkg-plist
@@ -11,7 +11,6 @@ bin/coqdoc
bin/coqnative
bin/coqpp
bin/coqtimelog2html
-bin/coqtop.opt
bin/coqtop
bin/coqtop.byte
bin/coqwc
@@ -21,6 +20,43 @@ bin/csdpcert
bin/ocamllibdep
bin/votour
%%IDE%%@dir etc/xdg/coq
+%%PORTDOCS%%%%DATADIR%%/coq-ssreflect.lang
+%%PORTDOCS%%%%DATADIR%%/coq.lang
+%%PORTDOCS%%%%DATADIR%%/coq.png
+%%PORTDOCS%%%%DATADIR%%/coq_style.xml
+@comment %%PORTDOCS%%%%DOCSDIR%%/FAQ-CoqIde
+@comment %%EMACS_SITE_LISPDIR%%/coq/coq-font-lock.el
+@comment %%EMACS_SITE_LISPDIR%%/coq/coq-inferior.el
+@comment %%EMACS_SITE_LISPDIR%%/coq/gallina-db.el
+@comment %%EMACS_SITE_LISPDIR%%/coq/gallina-syntax.el
+@comment %%EMACS_SITE_LISPDIR%%/coq/gallina.el
+@comment %%PORTDOCS%%%%EMACS_SITE_LISPDIR%%/coqdoc.sty
+%%DATADIR%%/default.bindings
+share/doc/ocaml/coq-core/LICENSE
+share/doc/ocaml/coq-core/README.md
+share/doc/ocaml/coq-stdlib/LICENSE
+share/doc/ocaml/coq-stdlib/README.md
+share/doc/ocaml/coq/LICENSE
+share/doc/ocaml/coq/README.md
+share/doc/ocaml/coq/odoc-pages/index.mld
+share/doc/ocaml/coqide-server/LICENSE
+share/doc/ocaml/coqide-server/README.md
+share/doc/ocaml/coqide/FAQ
+share/doc/ocaml/coqide/LICENSE
+share/doc/ocaml/coqide/README.md
+share/doc/ocaml/coqide/odoc-pages/index.mld
+share/man/man1/coq-tex.1.gz
+share/man/man1/coq_makefile.1.gz
+share/man/man1/coqc.1.gz
+share/man/man1/coqchk.1.gz
+share/man/man1/coqdep.1.gz
+share/man/man1/coqdoc.1.gz
+share/man/man1/coqide.1.gz
+share/man/man1/coqnative.1.gz
+share/man/man1/coqtop.byte.1.gz
+share/man/man1/coqtop.1.gz
+share/man/man1/coqwc.1.gz
+%%PORTDOCS%%%%TEXMFDIR%%/tex/latex/misc/coqdoc.sty
%%OCAML_SITELIBDIR%%/coq-core/META
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.a
%%OCAML_SITELIBDIR%%/coq-core/boot/boot.cma
@@ -54,6 +90,80 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/boot/usage.mli
%%OCAML_SITELIBDIR%%/coq-core/boot/util.ml
%%OCAML_SITELIBDIR%%/coq-core/boot/util.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/analyze.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/analyze.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/check.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/check.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/checkFlags.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/checkFlags.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/checkInductive.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/checkInductive.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/checkTypes.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/checkTypes.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/check_stat.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/check_stat.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/checker.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/checker.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.a
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.cma
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.cmxa
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.cmxs
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Analyze.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Analyze.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Analyze.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Analyze.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Check.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Check.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Check.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Check.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckFlags.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckFlags.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckFlags.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckFlags.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckInductive.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckInductive.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckInductive.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckInductive.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckTypes.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckTypes.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckTypes.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__CheckTypes.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Check_stat.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Check_stat.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Check_stat.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Check_stat.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Checker.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Checker.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Checker.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Checker.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Mod_checking.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Mod_checking.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Mod_checking.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Mod_checking.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Safe_checking.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Safe_checking.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Safe_checking.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Safe_checking.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Validate.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Validate.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Validate.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Validate.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Values.cmi
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Values.cmt
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Values.cmti
+%%OCAML_SITELIBDIR%%/coq-core/checklib/coq_checklib__Values.cmx
+%%OCAML_SITELIBDIR%%/coq-core/checklib/mod_checking.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/mod_checking.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/safe_checking.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/safe_checking.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/validate.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/validate.mli
+%%OCAML_SITELIBDIR%%/coq-core/checklib/values.ml
+%%OCAML_SITELIBDIR%%/coq-core/checklib/values.mli
%%OCAML_SITELIBDIR%%/coq-core/clib/cArray.cmi
%%OCAML_SITELIBDIR%%/coq-core/clib/cArray.cmt
%%OCAML_SITELIBDIR%%/coq-core/clib/cArray.cmti
@@ -169,12 +279,24 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/clib/int.cmx
%%OCAML_SITELIBDIR%%/coq-core/clib/int.ml
%%OCAML_SITELIBDIR%%/coq-core/clib/int.mli
+%%OCAML_SITELIBDIR%%/coq-core/clib/memprof_coq.cmi
+%%OCAML_SITELIBDIR%%/coq-core/clib/memprof_coq.cmt
+%%OCAML_SITELIBDIR%%/coq-core/clib/memprof_coq.cmti
+%%OCAML_SITELIBDIR%%/coq-core/clib/memprof_coq.cmx
+%%OCAML_SITELIBDIR%%/coq-core/clib/memprof_coq.ml
+%%OCAML_SITELIBDIR%%/coq-core/clib/memprof_coq.mli
%%OCAML_SITELIBDIR%%/coq-core/clib/monad.cmi
%%OCAML_SITELIBDIR%%/coq-core/clib/monad.cmt
%%OCAML_SITELIBDIR%%/coq-core/clib/monad.cmti
%%OCAML_SITELIBDIR%%/coq-core/clib/monad.cmx
%%OCAML_SITELIBDIR%%/coq-core/clib/monad.ml
%%OCAML_SITELIBDIR%%/coq-core/clib/monad.mli
+%%OCAML_SITELIBDIR%%/coq-core/clib/mutex_aux.cmi
+%%OCAML_SITELIBDIR%%/coq-core/clib/mutex_aux.cmt
+%%OCAML_SITELIBDIR%%/coq-core/clib/mutex_aux.cmti
+%%OCAML_SITELIBDIR%%/coq-core/clib/mutex_aux.cmx
+%%OCAML_SITELIBDIR%%/coq-core/clib/mutex_aux.ml
+%%OCAML_SITELIBDIR%%/coq-core/clib/mutex_aux.mli
%%OCAML_SITELIBDIR%%/coq-core/clib/neList.cmi
%%OCAML_SITELIBDIR%%/coq-core/clib/neList.cmt
%%OCAML_SITELIBDIR%%/coq-core/clib/neList.cmti
@@ -259,6 +381,12 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/clib/unionfind.cmx
%%OCAML_SITELIBDIR%%/coq-core/clib/unionfind.ml
%%OCAML_SITELIBDIR%%/coq-core/clib/unionfind.mli
+%%OCAML_SITELIBDIR%%/coq-core/config/byte/byte_config.cma
+%%OCAML_SITELIBDIR%%/coq-core/config/byte/coq_byte_config.cmi
+%%OCAML_SITELIBDIR%%/coq-core/config/byte/coq_byte_config.cmt
+%%OCAML_SITELIBDIR%%/coq-core/config/byte/coq_byte_config.cmti
+%%OCAML_SITELIBDIR%%/coq-core/config/byte/coq_byte_config.ml
+%%OCAML_SITELIBDIR%%/coq-core/config/byte/coq_byte_config.mli
%%OCAML_SITELIBDIR%%/coq-core/config/config.a
%%OCAML_SITELIBDIR%%/coq-core/config/config.cma
%%OCAML_SITELIBDIR%%/coq-core/config/config.cmxa
@@ -279,6 +407,36 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/coqworkmgrapi/coqworkmgrlib.cma
%%OCAML_SITELIBDIR%%/coq-core/coqworkmgrapi/coqworkmgrlib.cmxa
%%OCAML_SITELIBDIR%%/coq-core/coqworkmgrapi/coqworkmgrlib.cmxs
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.a
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.cma
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.cmi
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.cmt
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.cmti
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.cmx
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.cmxa
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.cmxs
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.ml
+%%OCAML_SITELIBDIR%%/coq-core/debugger_support/debugger_support.mli
+%%OCAML_SITELIBDIR%%/coq-core/dev/dev.a
+%%OCAML_SITELIBDIR%%/coq-core/dev/dev.cma
+%%OCAML_SITELIBDIR%%/coq-core/dev/dev.cmxa
+%%OCAML_SITELIBDIR%%/coq-core/dev/dev.cmxs
+%%OCAML_SITELIBDIR%%/coq-core/dev/ml_toplevel/include
+%%OCAML_SITELIBDIR%%/coq-core/dev/ml_toplevel/include_directories
+%%OCAML_SITELIBDIR%%/coq-core/dev/ml_toplevel/include_printers
+%%OCAML_SITELIBDIR%%/coq-core/dev/ml_toplevel/include_utilities
+%%OCAML_SITELIBDIR%%/coq-core/dev/top_printers.cmi
+%%OCAML_SITELIBDIR%%/coq-core/dev/top_printers.cmt
+%%OCAML_SITELIBDIR%%/coq-core/dev/top_printers.cmti
+%%OCAML_SITELIBDIR%%/coq-core/dev/top_printers.cmx
+%%OCAML_SITELIBDIR%%/coq-core/dev/top_printers.ml
+%%OCAML_SITELIBDIR%%/coq-core/dev/top_printers.mli
+%%OCAML_SITELIBDIR%%/coq-core/dev/vm_printers.cmi
+%%OCAML_SITELIBDIR%%/coq-core/dev/vm_printers.cmt
+%%OCAML_SITELIBDIR%%/coq-core/dev/vm_printers.cmti
+%%OCAML_SITELIBDIR%%/coq-core/dev/vm_printers.cmx
+%%OCAML_SITELIBDIR%%/coq-core/dev/vm_printers.ml
+%%OCAML_SITELIBDIR%%/coq-core/dev/vm_printers.mli
%%OCAML_SITELIBDIR%%/coq-core/dllcoqrun_stubs.so
%%OCAML_SITELIBDIR%%/coq-core/dune-package
%%OCAML_SITELIBDIR%%/coq-core/engine/eConstr.cmi
@@ -333,6 +491,12 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/engine/nameops.cmx
%%OCAML_SITELIBDIR%%/coq-core/engine/nameops.ml
%%OCAML_SITELIBDIR%%/coq-core/engine/nameops.mli
+%%OCAML_SITELIBDIR%%/coq-core/engine/profile_tactic.cmi
+%%OCAML_SITELIBDIR%%/coq-core/engine/profile_tactic.cmt
+%%OCAML_SITELIBDIR%%/coq-core/engine/profile_tactic.cmti
+%%OCAML_SITELIBDIR%%/coq-core/engine/profile_tactic.cmx
+%%OCAML_SITELIBDIR%%/coq-core/engine/profile_tactic.ml
+%%OCAML_SITELIBDIR%%/coq-core/engine/profile_tactic.mli
%%OCAML_SITELIBDIR%%/coq-core/engine/proofview.cmi
%%OCAML_SITELIBDIR%%/coq-core/engine/proofview.cmt
%%OCAML_SITELIBDIR%%/coq-core/engine/proofview.cmti
@@ -742,12 +906,24 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/kernel/parray.cmx
%%OCAML_SITELIBDIR%%/coq-core/kernel/parray.ml
%%OCAML_SITELIBDIR%%/coq-core/kernel/parray.mli
+%%OCAML_SITELIBDIR%%/coq-core/kernel/partial_subst.cmi
+%%OCAML_SITELIBDIR%%/coq-core/kernel/partial_subst.cmt
+%%OCAML_SITELIBDIR%%/coq-core/kernel/partial_subst.cmti
+%%OCAML_SITELIBDIR%%/coq-core/kernel/partial_subst.cmx
+%%OCAML_SITELIBDIR%%/coq-core/kernel/partial_subst.ml
+%%OCAML_SITELIBDIR%%/coq-core/kernel/partial_subst.mli
%%OCAML_SITELIBDIR%%/coq-core/kernel/primred.cmi
%%OCAML_SITELIBDIR%%/coq-core/kernel/primred.cmt
%%OCAML_SITELIBDIR%%/coq-core/kernel/primred.cmti
%%OCAML_SITELIBDIR%%/coq-core/kernel/primred.cmx
%%OCAML_SITELIBDIR%%/coq-core/kernel/primred.ml
%%OCAML_SITELIBDIR%%/coq-core/kernel/primred.mli
+%%OCAML_SITELIBDIR%%/coq-core/kernel/pstring.cmi
+%%OCAML_SITELIBDIR%%/coq-core/kernel/pstring.cmt
+%%OCAML_SITELIBDIR%%/coq-core/kernel/pstring.cmti
+%%OCAML_SITELIBDIR%%/coq-core/kernel/pstring.cmx
+%%OCAML_SITELIBDIR%%/coq-core/kernel/pstring.ml
+%%OCAML_SITELIBDIR%%/coq-core/kernel/pstring.mli
%%OCAML_SITELIBDIR%%/coq-core/kernel/redFlags.cmi
%%OCAML_SITELIBDIR%%/coq-core/kernel/redFlags.cmt
%%OCAML_SITELIBDIR%%/coq-core/kernel/redFlags.cmti
@@ -895,6 +1071,12 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlambda.cmx
%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlambda.ml
%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlambda.mli
+%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlibrary.cmi
+%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlibrary.cmt
+%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlibrary.cmti
+%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlibrary.cmx
+%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlibrary.ml
+%%OCAML_SITELIBDIR%%/coq-core/kernel/vmlibrary.mli
%%OCAML_SITELIBDIR%%/coq-core/kernel/vmopcodes.cmi
%%OCAML_SITELIBDIR%%/coq-core/kernel/vmopcodes.cmt
%%OCAML_SITELIBDIR%%/coq-core/kernel/vmopcodes.cmti
@@ -943,12 +1125,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/lib/cErrors.cmx
%%OCAML_SITELIBDIR%%/coq-core/lib/cErrors.ml
%%OCAML_SITELIBDIR%%/coq-core/lib/cErrors.mli
-%%OCAML_SITELIBDIR%%/coq-core/lib/cProfile.cmi
-%%OCAML_SITELIBDIR%%/coq-core/lib/cProfile.cmt
-%%OCAML_SITELIBDIR%%/coq-core/lib/cProfile.cmti
-%%OCAML_SITELIBDIR%%/coq-core/lib/cProfile.cmx
-%%OCAML_SITELIBDIR%%/coq-core/lib/cProfile.ml
-%%OCAML_SITELIBDIR%%/coq-core/lib/cProfile.mli
%%OCAML_SITELIBDIR%%/coq-core/lib/cWarnings.cmi
%%OCAML_SITELIBDIR%%/coq-core/lib/cWarnings.cmt
%%OCAML_SITELIBDIR%%/coq-core/lib/cWarnings.cmti
@@ -1073,6 +1249,12 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/lib/system.cmx
%%OCAML_SITELIBDIR%%/coq-core/lib/system.ml
%%OCAML_SITELIBDIR%%/coq-core/lib/system.mli
+%%OCAML_SITELIBDIR%%/coq-core/lib/userWarn.cmi
+%%OCAML_SITELIBDIR%%/coq-core/lib/userWarn.cmt
+%%OCAML_SITELIBDIR%%/coq-core/lib/userWarn.cmti
+%%OCAML_SITELIBDIR%%/coq-core/lib/userWarn.cmx
+%%OCAML_SITELIBDIR%%/coq-core/lib/userWarn.ml
+%%OCAML_SITELIBDIR%%/coq-core/lib/userWarn.mli
%%OCAML_SITELIBDIR%%/coq-core/lib/util.cmi
%%OCAML_SITELIBDIR%%/coq-core/lib/util.cmt
%%OCAML_SITELIBDIR%%/coq-core/lib/util.cmti
@@ -1560,10 +1742,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Pptactic.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Pptactic.cmti
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Pptactic.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Profile_ltac.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Profile_ltac.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Profile_ltac.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Profile_ltac.cmx
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmi
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmti
@@ -1585,9 +1763,7 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacenv.cmti
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacenv.cmx
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacexpr.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacexpr.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacexpr.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacexpr.cmx
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacintern.cmi
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacintern.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/ltac_plugin__Tacintern.cmti
@@ -1616,8 +1792,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/pltac.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/pptactic.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/pptactic.mli
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/profile_ltac.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/profile_ltac.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/profile_ltac_tactics.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/profile_ltac_tactics.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/tacarg.ml
@@ -1628,7 +1802,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/tacentries.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/tacenv.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/tacenv.mli
-%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/tacexpr.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/tacexpr.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/tacintern.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac/tacintern.mli
@@ -1726,6 +1899,10 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmti
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/ltac2_plugin__Tac2val.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/ltac2_plugin__Tac2val.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/ltac2_plugin__Tac2val.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/ltac2_plugin__Tac2val.cmx
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/tac2bt.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/tac2bt.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/tac2core.ml
@@ -1761,6 +1938,40 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/tac2types.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/tac2typing_env.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/tac2typing_env.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/tac2val.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2/tac2val.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/g_ltac2_ltac1.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/g_ltac2_ltac1.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin.a
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cma
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxa
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxs
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/tac2core_ltac1.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/tac2core_ltac1.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/tac2quote_ltac1.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/tac2quote_ltac1.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/tac2stdlib_ltac1.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/ltac2_ltac1/tac2stdlib_ltac1.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/certificate.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/certificate.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/coq_micromega.ml
@@ -1771,8 +1982,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/itv.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/linsolve.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/linsolve.mli
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin.a
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin.cma
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin.cmi
@@ -1801,18 +2010,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Linsolve.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Linsolve.cmti
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Linsolve.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Micromega.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Micromega.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Micromega.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Micromega.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Mutils.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Mutils.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Mutils.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Mutils.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__NumCompat.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__NumCompat.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__NumCompat.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__NumCompat.cmx
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Persistent_cache.cmi
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Persistent_cache.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Persistent_cache.cmti
@@ -1825,40 +2022,62 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Simplex.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Simplex.cmti
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Simplex.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos_lib.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos_lib.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos_lib.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos_lib.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos_types.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos_types.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos_types.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Sos_types.cmx
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Vect.cmi
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Vect.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Vect.cmti
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/micromega_plugin__Vect.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/mutils.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/mutils.mli
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/numCompat.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/numCompat.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/persistent_cache.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/persistent_cache.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/polynomial.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/polynomial.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/simplex.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/simplex.mli
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/sos.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/sos.mli
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/sos_lib.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/sos_lib.mli
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/sos_types.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/sos_types.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/vect.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega/vect.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin.a
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin.cma
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin.cmxa
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin.cmxs
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Micromega.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Micromega.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Micromega.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Micromega.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Mutils.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Mutils.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Mutils.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Mutils.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__NumCompat.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__NumCompat.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__NumCompat.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__NumCompat.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos_types.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos_types.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos_types.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/micromega_core_plugin__Sos_types.cmx
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/mutils.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/mutils.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/numCompat.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/numCompat.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/sos.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/sos.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/sos_lib.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/sos_lib.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/sos_types.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/micromega_core/sos_types.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/nsatz/g_nsatz.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/nsatz/g_nsatz.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/nsatz/ideal.ml
@@ -1899,8 +2118,8 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/nsatz/utile.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/g_number_string.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/g_number_string.mli
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string.ml
+%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin.a
%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin.cma
%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin.cmi
@@ -1913,16 +2132,10 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmt
%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmti
%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__Number.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__Number.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__Number.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__Number.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__String_notation.cmi
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__String_notation.cmt
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__String_notation.cmti
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__String_notation.cmx
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/string_notation.ml
-%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/string_notation.mli
+%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmi
+%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmt
+%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmti
+%%OCAML_SITELIBDIR%%/coq-core/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmx
%%OCAML_SITELIBDIR%%/coq-core/plugins/ring/g_ring.ml
%%OCAML_SITELIBDIR%%/coq-core/plugins/ring/g_ring.mli
%%OCAML_SITELIBDIR%%/coq-core/plugins/ring/ring.ml
@@ -2250,6 +2463,12 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/pretyping/coercionops.cmx
%%OCAML_SITELIBDIR%%/coq-core/pretyping/coercionops.ml
%%OCAML_SITELIBDIR%%/coq-core/pretyping/coercionops.mli
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/combinators.cmi
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/combinators.cmt
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/combinators.cmti
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/combinators.cmx
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/combinators.ml
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/combinators.mli
%%OCAML_SITELIBDIR%%/coq-core/pretyping/constr_matching.cmi
%%OCAML_SITELIBDIR%%/coq-core/pretyping/constr_matching.cmt
%%OCAML_SITELIBDIR%%/coq-core/pretyping/constr_matching.cmti
@@ -2262,6 +2481,12 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/pretyping/detyping.cmx
%%OCAML_SITELIBDIR%%/coq-core/pretyping/detyping.ml
%%OCAML_SITELIBDIR%%/coq-core/pretyping/detyping.mli
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/evaluable.cmi
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/evaluable.cmt
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/evaluable.cmti
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/evaluable.cmx
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/evaluable.ml
+%%OCAML_SITELIBDIR%%/coq-core/pretyping/evaluable.mli
%%OCAML_SITELIBDIR%%/coq-core/pretyping/evarconv.cmi
%%OCAML_SITELIBDIR%%/coq-core/pretyping/evarconv.cmt
%%OCAML_SITELIBDIR%%/coq-core/pretyping/evarconv.cmti
@@ -2600,12 +2825,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/stm/vcs.cmx
%%OCAML_SITELIBDIR%%/coq-core/stm/vcs.ml
%%OCAML_SITELIBDIR%%/coq-core/stm/vcs.mli
-%%OCAML_SITELIBDIR%%/coq-core/stm/vio_checking.cmi
-%%OCAML_SITELIBDIR%%/coq-core/stm/vio_checking.cmt
-%%OCAML_SITELIBDIR%%/coq-core/stm/vio_checking.cmti
-%%OCAML_SITELIBDIR%%/coq-core/stm/vio_checking.cmx
-%%OCAML_SITELIBDIR%%/coq-core/stm/vio_checking.ml
-%%OCAML_SITELIBDIR%%/coq-core/stm/vio_checking.mli
%%OCAML_SITELIBDIR%%/coq-core/stm/workerPool.cmi
%%OCAML_SITELIBDIR%%/coq-core/stm/workerPool.cmt
%%OCAML_SITELIBDIR%%/coq-core/stm/workerPool.cmti
@@ -2822,16 +3041,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/tools/make-both-single-timing-files.py
%%OCAML_SITELIBDIR%%/coq-core/tools/make-both-time-files.py
%%OCAML_SITELIBDIR%%/coq-core/tools/make-one-time-file.py
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.a
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.cma
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.cmi
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.cmt
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.cmti
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.cmx
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.cmxa
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.cmxs
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.ml
-%%OCAML_SITELIBDIR%%/coq-core/top_printers/top_printers.mli
%%OCAML_SITELIBDIR%%/coq-core/toplevel/ccompile.cmi
%%OCAML_SITELIBDIR%%/coq-core/toplevel/ccompile.cmt
%%OCAML_SITELIBDIR%%/coq-core/toplevel/ccompile.cmti
@@ -2908,12 +3117,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/toplevel/vernac.cmx
%%OCAML_SITELIBDIR%%/coq-core/toplevel/vernac.ml
%%OCAML_SITELIBDIR%%/coq-core/toplevel/vernac.mli
-%%OCAML_SITELIBDIR%%/coq-core/toplevel/vio_compile.cmi
-%%OCAML_SITELIBDIR%%/coq-core/toplevel/vio_compile.cmt
-%%OCAML_SITELIBDIR%%/coq-core/toplevel/vio_compile.cmti
-%%OCAML_SITELIBDIR%%/coq-core/toplevel/vio_compile.cmx
-%%OCAML_SITELIBDIR%%/coq-core/toplevel/vio_compile.ml
-%%OCAML_SITELIBDIR%%/coq-core/toplevel/vio_compile.mli
%%OCAML_SITELIBDIR%%/coq-core/toplevel/workerLoop.cmi
%%OCAML_SITELIBDIR%%/coq-core/toplevel/workerLoop.cmt
%%OCAML_SITELIBDIR%%/coq-core/toplevel/workerLoop.cmti
@@ -3010,6 +3213,12 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/vernac/comProgramFixpoint.cmx
%%OCAML_SITELIBDIR%%/coq-core/vernac/comProgramFixpoint.ml
%%OCAML_SITELIBDIR%%/coq-core/vernac/comProgramFixpoint.mli
+%%OCAML_SITELIBDIR%%/coq-core/vernac/comRewriteRule.cmi
+%%OCAML_SITELIBDIR%%/coq-core/vernac/comRewriteRule.cmt
+%%OCAML_SITELIBDIR%%/coq-core/vernac/comRewriteRule.cmti
+%%OCAML_SITELIBDIR%%/coq-core/vernac/comRewriteRule.cmx
+%%OCAML_SITELIBDIR%%/coq-core/vernac/comRewriteRule.ml
+%%OCAML_SITELIBDIR%%/coq-core/vernac/comRewriteRule.mli
%%OCAML_SITELIBDIR%%/coq-core/vernac/comSearch.cmi
%%OCAML_SITELIBDIR%%/coq-core/vernac/comSearch.cmt
%%OCAML_SITELIBDIR%%/coq-core/vernac/comSearch.cmti
@@ -3076,6 +3285,12 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq-core/vernac/g_proofs.cmx
%%OCAML_SITELIBDIR%%/coq-core/vernac/g_proofs.ml
%%OCAML_SITELIBDIR%%/coq-core/vernac/g_proofs.mli
+%%OCAML_SITELIBDIR%%/coq-core/vernac/g_redexpr.cmi
+%%OCAML_SITELIBDIR%%/coq-core/vernac/g_redexpr.cmt
+%%OCAML_SITELIBDIR%%/coq-core/vernac/g_redexpr.cmti
+%%OCAML_SITELIBDIR%%/coq-core/vernac/g_redexpr.cmx
+%%OCAML_SITELIBDIR%%/coq-core/vernac/g_redexpr.ml
+%%OCAML_SITELIBDIR%%/coq-core/vernac/g_redexpr.mli
%%OCAML_SITELIBDIR%%/coq-core/vernac/g_vernac.cmi
%%OCAML_SITELIBDIR%%/coq-core/vernac/g_vernac.cmt
%%OCAML_SITELIBDIR%%/coq-core/vernac/g_vernac.cmti
@@ -3490,20 +3705,16 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/Classes/SetoidTactics.vos
%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmi
%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs
-%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_Coq817.cmi
-%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_Coq817.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_Coq818.cmi
%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_Coq818.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_Coq819.cmi
%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_Coq819.cmxs
+%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_Coq820.cmi
+%%OCAML_SITELIBDIR%%/coq/theories/Compat/.coq-native/NCoq_Compat_Coq820.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/Compat/AdmitAxiom.glob
%%OCAML_SITELIBDIR%%/coq/theories/Compat/AdmitAxiom.v
%%OCAML_SITELIBDIR%%/coq/theories/Compat/AdmitAxiom.vo
%%OCAML_SITELIBDIR%%/coq/theories/Compat/AdmitAxiom.vos
-%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq817.glob
-%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq817.v
-%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq817.vo
-%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq817.vos
%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq818.glob
%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq818.v
%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq818.vo
@@ -3512,6 +3723,10 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq819.v
%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq819.vo
%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq819.vos
+%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq820.glob
+%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq820.v
+%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq820.vo
+%%OCAML_SITELIBDIR%%/coq/theories/Compat/Coq820.vos
%%OCAML_SITELIBDIR%%/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi
%%OCAML_SITELIBDIR%%/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmi
@@ -4132,10 +4347,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_NArith.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ndec.cmi
%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ndec.cmxs
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ndigits.cmi
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ndigits.cmxs
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ndist.cmi
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ndist.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ndiv_def.cmi
%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ndiv_def.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/NArith/.coq-native/NCoq_NArith_Ngcd_def.cmi
@@ -4160,14 +4371,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndec.v
%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndec.vo
%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndec.vos
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndigits.glob
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndigits.v
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndigits.vo
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndigits.vos
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndist.glob
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndist.v
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndist.vo
-%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndist.vos
%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndiv_def.glob
%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndiv_def.v
%%OCAML_SITELIBDIR%%/coq/theories/NArith/Ndiv_def.vo
@@ -5582,12 +5785,16 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_BinaryString.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmi
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_Byte.cmxs
-%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmi
-%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_ByteVector.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmi
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_HexString.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmi
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_OctalString.cmxs
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_PString.cmi
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_PString.cmxs
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_PrimString.cmi
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_PrimString.cmxs
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_PrimStringAxioms.cmi
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_PrimStringAxioms.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmi
%%OCAML_SITELIBDIR%%/coq/theories/Strings/.coq-native/NCoq_Strings_String.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/Strings/Ascii.glob
@@ -5602,10 +5809,6 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/Strings/Byte.v
%%OCAML_SITELIBDIR%%/coq/theories/Strings/Byte.vo
%%OCAML_SITELIBDIR%%/coq/theories/Strings/Byte.vos
-%%OCAML_SITELIBDIR%%/coq/theories/Strings/ByteVector.glob
-%%OCAML_SITELIBDIR%%/coq/theories/Strings/ByteVector.v
-%%OCAML_SITELIBDIR%%/coq/theories/Strings/ByteVector.vo
-%%OCAML_SITELIBDIR%%/coq/theories/Strings/ByteVector.vos
%%OCAML_SITELIBDIR%%/coq/theories/Strings/HexString.glob
%%OCAML_SITELIBDIR%%/coq/theories/Strings/HexString.v
%%OCAML_SITELIBDIR%%/coq/theories/Strings/HexString.vo
@@ -5614,6 +5817,18 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/Strings/OctalString.v
%%OCAML_SITELIBDIR%%/coq/theories/Strings/OctalString.vo
%%OCAML_SITELIBDIR%%/coq/theories/Strings/OctalString.vos
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PString.glob
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PString.v
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PString.vo
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PString.vos
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PrimString.glob
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PrimString.v
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PrimString.vo
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PrimString.vos
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PrimStringAxioms.glob
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PrimStringAxioms.v
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PrimStringAxioms.vo
+%%OCAML_SITELIBDIR%%/coq/theories/Strings/PrimStringAxioms.vos
%%OCAML_SITELIBDIR%%/coq/theories/Strings/String.glob
%%OCAML_SITELIBDIR%%/coq/theories/Strings/String.v
%%OCAML_SITELIBDIR%%/coq/theories/Strings/String.vo
@@ -6030,6 +6245,8 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlPArray.cmi
%%OCAML_SITELIBDIR%%/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlPArray.cmxs
+%%OCAML_SITELIBDIR%%/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlPString.cmi
+%%OCAML_SITELIBDIR%%/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOCamlPString.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi
%%OCAML_SITELIBDIR%%/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
%%OCAML_SITELIBDIR%%/coq/theories/extraction/.coq-native/NCoq_extraction_ExtrOcamlChar.cmi
@@ -6094,6 +6311,10 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOCamlPArray.v
%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOCamlPArray.vo
%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOCamlPArray.vos
+%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOCamlPString.glob
+%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOCamlPString.v
+%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOCamlPString.vo
+%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOCamlPString.vos
%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOcamlBasic.glob
%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOcamlBasic.v
%%OCAML_SITELIBDIR%%/coq/theories/extraction/ExtrOcamlBasic.vo
@@ -6610,6 +6831,8 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/.coq-native/NLtac2_Printf.cmxs
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/.coq-native/NLtac2_Proj.cmi
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/.coq-native/NLtac2_Proj.cmxs
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pstring.cmi
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/.coq-native/NLtac2_Pstring.cmxs
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/.coq-native/NLtac2_RedFlags.cmi
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/.coq-native/NLtac2_RedFlags.cmxs
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/.coq-native/NLtac2_Ref.cmi
@@ -6638,10 +6861,16 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Char.vos
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq818.cmi
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq818.cmxs
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq819.cmi
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/.coq-native/NLtac2_Compat_Coq819.cmxs
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/Coq818.glob
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/Coq818.v
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/Coq818.vo
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/Coq818.vos
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/Coq819.glob
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/Coq819.v
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/Coq819.vo
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Compat/Coq819.vos
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Constant.glob
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Constant.v
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Constant.vo
@@ -6742,6 +6971,10 @@ bin/votour
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Proj.v
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Proj.vo
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Proj.vos
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Pstring.glob
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Pstring.v
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Pstring.vo
+%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/Pstring.vos
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/RedFlags.glob
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/RedFlags.v
%%OCAML_SITELIBDIR%%/coq/user-contrib/Ltac2/RedFlags.vo
@@ -6829,41 +7062,3 @@ bin/votour
%%IDE%%%%OCAML_SITELIBDIR%%/coqide/META
%%IDE%%%%OCAML_SITELIBDIR%%/coqide/dune-package
%%IDE%%%%OCAML_SITELIBDIR%%/coqide/opam
-%%PORTDOCS%%%%DATADIR%%/coq-ssreflect.lang
-%%PORTDOCS%%%%DATADIR%%/coq.lang
-%%PORTDOCS%%%%DATADIR%%/coq.png
-%%PORTDOCS%%%%DATADIR%%/coq_style.xml
-@comment %%PORTDOCS%%%%DOCSDIR%%/FAQ-CoqIde
-@comment %%EMACS_SITE_LISPDIR%%/coq/coq-font-lock.el
-@comment %%EMACS_SITE_LISPDIR%%/coq/coq-inferior.el
-@comment %%EMACS_SITE_LISPDIR%%/coq/gallina-db.el
-@comment %%EMACS_SITE_LISPDIR%%/coq/gallina-syntax.el
-@comment %%EMACS_SITE_LISPDIR%%/coq/gallina.el
-@comment %%PORTDOCS%%%%EMACS_SITE_LISPDIR%%/coqdoc.sty
-%%DATADIR%%/default.bindings
-share/doc/ocaml/coq-core/LICENSE
-share/doc/ocaml/coq-core/README.md
-share/doc/ocaml/coq-stdlib/LICENSE
-share/doc/ocaml/coq-stdlib/README.md
-share/doc/ocaml/coq/LICENSE
-share/doc/ocaml/coq/README.md
-share/doc/ocaml/coq/odoc-pages/index.mld
-share/doc/ocaml/coqide-server/LICENSE
-share/doc/ocaml/coqide-server/README.md
-share/doc/ocaml/coqide/FAQ
-share/doc/ocaml/coqide/LICENSE
-share/doc/ocaml/coqide/README.md
-share/doc/ocaml/coqide/odoc-pages/index.mld
-share/man/man1/coq-tex.1.gz
-share/man/man1/coq_makefile.1.gz
-share/man/man1/coqc.1.gz
-share/man/man1/coqchk.1.gz
-share/man/man1/coqdep.1.gz
-share/man/man1/coqdoc.1.gz
-share/man/man1/coqide.1.gz
-share/man/man1/coqnative.1.gz
-share/man/man1/coqtop.1.gz
-share/man/man1/coqtop.byte.1.gz
-share/man/man1/coqtop.opt.1.gz
-share/man/man1/coqwc.1.gz
-%%PORTDOCS%%%%TEXMFDIR%%/tex/latex/misc/coqdoc.sty