Updated coq to latest version, 8.6. Changes include:

Changes from V8.6beta1 to V8.6 ============================== Kernel - Fixed critical bug #5248 in VM long multiplication on 32-bit architectures. Was there only since 8.6beta1, so no stable release impacted. Other bug fixes in universes, type class shelving,... Changes from V8.5 to V8.6beta1 ============================== Kernel - A new, faster state-of-the-art universe constraint checker. Specification language - Giving implicit arguments explicitly to a constant with multiple choices of implicit arguments does not break any more insertion of further maximal implicit arguments. - Ability to put any pattern in binders, prefixed by quote, e.g. "fun '(a,b) => ...", "λ '(a,(b,c)), ...", "Definition foo '(x,y) := ...". It expands into a "let 'pattern := ..." Tactics - Flag "Bracketing Last Introduction Pattern" is now on by default. - Flag "Regular Subst Tactic" is now on by default: it respects the initial order of hypothesis, it contracts cycles, it unfolds no local definitions (common source of incompatibilities, fixable by "Unset Regular Subst Tactic"). - New flag "Refolding Reduction", now disabled by default, which turns on refolding of constants/fixpoints (as in cbn) during the reductions done during type inference and tactic retyping. Can be extremely expensive. When set off, this recovers the 8.4 behaviour of unification and type inference. Potential source of incompatibility with 8.5 developments (the option is set on in Compat/Coq85.v). - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract tactical w.r.t. variables appearing in the body of the proof. On by default and deprecated. Minor source of incompatibility for code relying on the precise arguments of abstracted proofs. - Serious bugs are fixed in tactic "double induction" (source of incompatibilities as soon as the inductive types have dependencies in the type of their constructors; "double induction" remains however deprecated). - In introduction patterns of the form (pat1,...,patn), n should match the exact number of hypotheses introduced (except for local definitions for which pattern can be omitted, as in regular pattern-matching). - Tactic scopes in Ltac like constr: and ltac: now require parentheses around their argument. - Every generic argument type declares a tactic scope of the form "name:(...)" where name is the name of the argument. This generalizes the constr: and ltac: instances. - When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is given a free identifier, it is not bound in subsequent tactics anymore. In order to introduce a binding, use e.g. the "fresh" primitive instead (potential source of incompatibilities). - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac. - New goal selectors. Sets of goals can be selected by listing integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24. - For uniformity with "destruct"/"induction" and for a more natural behavior, "injection" can now work in place by activating option "Structural Injection". In this case, hypotheses are also put in the context in the natural left-to-right order and the hypothesis on which injection applies is cleared. - Tactic "contradiction" (hence "easy") now also solve goals with hypotheses of the form "~True" or "t<>t" (possible source of incompatibilities because of more successes in automation, but generally a more intuitive strategy). - Option "Injection On Proofs" was renamed "Keep Proof Equalities". When enabled, injection and inversion do not drop equalities between objects in Prop. Still disabled by default. - New tactics "notypeclasses refine" and "simple notypeclasses refine" that disallow typeclass resolution when typechecking their argument, for use in typeclass hints. - Integration of LtacProf, a profiler for Ltac. - Reduction tactics now accept more fine-grained flags: iota is now a shorthand for the new flags match, fix and cofix. - The ssreflect subterm selection algorithm is now accessible to tactic writers through the ssrmatching plugin. - When used as an argument of an ltac function, "auto" without "with" nor "using" clause now correctly uses only the core hint database by default. Hints - Revised the syntax of [Hint Cut] to follow standard notation for regexps. - Hint Mode now accepts "!" which means that the mode matches only if the argument's head is not an evar (it goes under applications, casts, and scrutinees of matches and projections). - Hints can now take an optional user-given pattern, used only by [typeclasses eauto] with the [Filtered Unification] option on. Typeclasses - Many new options and new engine based on the proof monad. The [typeclasses eauto] tactic is now a multi-goal, multi-success tactic. See reference manual for more information. It is planned to replace auto and eauto in the following version. The 8.5 resolution engine is still available to help solve compatibility issues. Program - The "Shrink Obligations" flag now applies to all obligations, not only those solved by the automatic tactic. - "Shrink Obligations" is on by default and deprecated. Minor source of incompatibility for code relying on the precise arguments of obligations. Notations - "Bind Scope" can once again bind "Funclass" and "Sortclass". General infrastructure - New configurable warning system which can be controlled with the vernacular command "Set Warnings", or, under coqc/coqtop, with the flag "-w". In particular, the default is now that warnings are printed by coqc. - In asynchronous mode, Coq is now capable of recovering from errors and continue processing the document. Tools - coqc accepts a -o option to specify the output file name - coqtop accepts --print-version to print Coq and OCaml versions in easy to parse format - Setting [Printing Dependent Evars Line] can be unset to disable the computation associated with printing the "dependent evars: " line in -emacs mode - Removed the -verbose-compat-notations flag and the corresponding Set Verbose Compat vernacular, since these warnings can now be silenced or turned into errors using "-w". XML protocol - message format has changed, see dev/doc/changes.txt for more details. Many bug fixes, minor changes and documentation improvements are not mentioned here. Changes from V8.5pl2 to V8.5pl3 =============================== Critical bugfix - #4876: Guard checker incompleteness when using primitive projections Other bugfixes - #4780: Induction with universe polymorphism on was creating ill-typed terms. - #4673: regression in setoid_rewrite, unfolding let-ins for type unification. - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain. - #4769: Anomaly with universe polymorphic schemes defined inside sections. - #3886: Program: duplicate obligations of mutual fixpoints. - #4994: Documentation typo. - #5008: Use the "md5" command on OpenBSD. - #5007: Do not assume the "TERM" environment variable is always set. - #4606: Output a break before a list only if there was an empty line. - #5001: metas not cleaned properly in clenv_refine_in. - #2336: incorrect glob data for module symbols (bug #2336). - #4832: Remove extraneous dot in error message. - Anomaly in printing a unification error message. - #4947: Options which take string arguments are not backwards compatible. - #4156: micromega cache files are now hidden files. - #4871: interrupting par:abstract kills coqtop. - #5043: [Admitted] lemmas pick up section variables. - Fix name of internal refine ("simple refine"). - #5062: probably a typo in Strict Proofs mode. - #5065: Anomaly: Not a proof by induction. - Restore native compiler optimizations, they were disabled since 8.5! - #5077: failure on typing a fixpoint with evars in its type. - Fix recursive notation bug. - #5095: non relevant too strict test in let-in abstraction. - Ensuring that the evar name is preserved by "rename". - #4887: confusion between using and with in documentation of firstorder. - Bug in subst with let-ins. - #4762: eauto weaker than auto. - Remove if_then_else (was buggy). Use tryif instead. - #4970: confusion between special "{" and non special "{{" in notations. - #4529: primitive projections unfolding. - #4416: Incorrect "Error: Incorrect number of goals". - #4863: abstract in typeclass hint fails. - #5123: unshelve can impact typeclass resolution - Fix a collision about the meta-variable ".." in recursive notations. - Fix printing of info_auto. - #3209: Not_found due to an occur-check cycle. - #5097: status of evars refined by "clear" in ltac: closed wrt evars. - #5150: Missing dependency of the test-suite subsystems in prerequisite. - Fix a bug in error printing of unif constraints - #3941: Do not stop propagation of signals when Coq is busy. - #4822: Incorrect assertion in cbn. - #3479 parsing of "{" and "}" when a keyword starts with "{" or "}". - #5127: Memory corruption with the VM. - #5102: bullets parsing broken by calls to parse_entry. Various documentation improvements Changes from V8.5pl1 to V8.5pl2 =============================== Critical bugfix - Checksums of .vo files dependencies were not correctly checked. - Unicode-to-ASCII translation was not injective, leading in a soundness bug in the native compiler. Other bugfixes - #4097: more efficient occur-check in presence of primitive projections - #4398: type_scope used consistently in "match goal". - #4450: eauto does not work with polymorphic lemmas - #4677: fix alpha-conversion in notations needing eta-expansion. - Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. - #4644: a regression in unification. - #4725: Function (Error: Conversion test raised an anomaly) and Program (Error: Cannot infer this placeholder of type) - #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings - #4752: CoqIDE crash on files not ended by ".v". - #4777: printing inefficiency with implicit arguments - #4818: "Admitted" fails due to undefined universe anomaly after calling "destruct" - #4823: remote counter: avoid thread race on sockets - #4841: -verbose flag changed semantics in 8.5, is much harder to use - #4851: [nsatz] cannot handle duplicated hypotheses - #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant of nsatz - #4880: [nsatz_compute] generates invalid certificates if given redundant hypotheses - #4881: synchronizing "Declare Implicit Tactic" with backtrack. - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. triggered by CoqIDE - #4069, #4718: congruence fails when universes are involved. Universes - Disallow silently dropping universe instances applied to variables (forward compatible) - Allow explicit universe instances on notations, when they can apply to the head reference of their expansion. Build infrastructure - New update on how to find camlp5 binary and library at configure time.
author: jaapb <jaapb> 2016-12-30 13:23:06 +0000
committer: jaapb <jaapb> 2016-12-30 13:23:06 +0000
commit: 40ffa23afb27611843446f19e713dc0bf76d9020 (patch)
tree: 6b0f4f66439c2e7cb191a3ace939fd685c091ef1 /lang
parent: 441c004edc347960b94a297f8de9854d7a308f49 (diff)
download: pkgsrc-40ffa23afb27611843446f19e713dc0bf76d9020.tar.gz
6 files changed, 164 insertions, 172 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index c1ad18241c3..05c9e90ce67 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.92 2016/12/04 05:17:31 ryoon Exp $
+# $NetBSD: Makefile,v 1.93 2016/12/30 13:23:06 jaapb Exp $
 #
 
-DISTNAME=	coq-8.5pl1
-PKGREVISION=	2
+DISTNAME=	coq-8.6
 CATEGORIES=	lang math
 MASTER_SITES=	http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
@@ -59,5 +58,4 @@ SUBST_FILES.fix-paths=	config/coq_config.ml
 SUBST_SED.fix-paths=	-e "s,${BUILDLINK_DIR},${PREFIX},g"
 
 .include "../../mk/pthread.buildlink3.mk"
-.include "../../lang/camlp5/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"
diff --git a/lang/coq/PLIST b/lang/coq/PLIST
index d9bf11cc798..f4bb52b1acd 100644
--- a/lang/coq/PLIST
+++ b/lang/coq/PLIST
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.19 2016/07/02 10:17:18 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.20 2016/12/30 13:23:06 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -12,10 +12,26 @@ bin/coqtop.byte
 bin/coqwc
 bin/coqworkmgr
 bin/gallina
-lib/coq/config/coq_config.cmi
+lib/coq/META
 lib/coq/dllcoqrun.so
+${PLIST.ocaml-opt}lib/coq/engine/engine.a
+lib/coq/engine/engine.cma
+${PLIST.ocaml-opt}lib/coq/engine/engine.cmxa
+lib/coq/engine/evarutil.cmi
+lib/coq/engine/evd.cmi
+lib/coq/engine/ftactic.cmi
+lib/coq/engine/geninterp.cmi
+lib/coq/engine/logic_monad.cmi
+lib/coq/engine/namegen.cmi
+lib/coq/engine/proofview.cmi
+lib/coq/engine/proofview_monad.cmi
+lib/coq/engine/sigma.cmi
+lib/coq/engine/termops.cmi
+lib/coq/engine/uState.cmi
+lib/coq/config/coq_config.cmi
 lib/coq/grammar/grammar.cma
 lib/coq/grammar/q_util.cmi
+lib/coq/grammar/compat5.cmo
 ${PLIST.coqide}lib/coq/ide/config_lexer.cmi
 ${PLIST.coqide}lib/coq/ide/coq.cmi
 ${PLIST.coqide}lib/coq/ide/coqOps.cmi
@@ -34,8 +50,10 @@ ${PLIST.coqide}lib/coq/ide/minilib.cmi
 ${PLIST.coqide}lib/coq/ide/nanoPG.cmi
 ${PLIST.coqide}lib/coq/ide/preferences.cmi
 ${PLIST.coqide}lib/coq/ide/project_file.cmi
+${PLIST.coqide}lib/coq/ide/richprinter.cmi
 ${PLIST.coqide}lib/coq/ide/sentence.cmi
 ${PLIST.coqide}lib/coq/ide/session.cmi
+${PLIST.coqide}lib/coq/ide/serialize.cmi
 ${PLIST.coqide}lib/coq/ide/tags.cmi
 ${PLIST.coqide}lib/coq/ide/utf8_convert.cmi
 ${PLIST.coqide}lib/coq/ide/utils/config_file.cmi
@@ -56,6 +74,9 @@ ${PLIST.coqide}lib/coq/ide/wg_ProofView.cmi
 ${PLIST.coqide}lib/coq/ide/wg_ScriptView.cmi
 ${PLIST.coqide}lib/coq/ide/wg_Segment.cmi
 ${PLIST.coqide}lib/coq/ide/xmlprotocol.cmi
+${PLIST.coqide}lib/coq/ide/xml_lexer.cmi
+${PLIST.coqide}lib/coq/ide/xml_parser.cmi
+${PLIST.coqide}lib/coq/ide/xml_printer.cmi
 lib/coq/interp/constrarg.cmi
 lib/coq/interp/constrexpr_ops.cmi
 lib/coq/interp/constrextern.cmi
@@ -88,10 +109,10 @@ lib/coq/intf/notation_term.cmi
 lib/coq/intf/pattern.cmi
 lib/coq/intf/tacexpr.cmi
 lib/coq/intf/vernacexpr.cmi
+lib/coq/kernel/cClosure.cmi
 lib/coq/kernel/cbytecodes.cmi
 lib/coq/kernel/cbytegen.cmi
 lib/coq/kernel/cemitcodes.cmi
-lib/coq/kernel/closure.cmi
 lib/coq/kernel/constr.cmi
 lib/coq/kernel/context.cmi
 lib/coq/kernel/conv_oracle.cmi
@@ -133,6 +154,7 @@ lib/coq/kernel/term.cmi
 lib/coq/kernel/term_typing.cmi
 lib/coq/kernel/type_errors.cmi
 lib/coq/kernel/typeops.cmi
+lib/coq/kernel/uGraph.cmi
 lib/coq/kernel/uint31.cmi
 lib/coq/kernel/univ.cmi
 lib/coq/kernel/vars.cmi
@@ -143,6 +165,7 @@ lib/coq/lib/backtrace.cmi
 lib/coq/lib/bigint.cmi
 lib/coq/lib/cArray.cmi
 lib/coq/lib/cEphemeron.cmi
+lib/coq/lib/cErrors.cmi
 lib/coq/lib/cList.cmi
 lib/coq/lib/cMap.cmi
 lib/coq/lib/cObj.cmi
@@ -152,6 +175,7 @@ lib/coq/lib/cStack.cmi
 lib/coq/lib/cString.cmi
 lib/coq/lib/cThread.cmi
 lib/coq/lib/cUnix.cmi
+lib/coq/lib/cWarnings.cmi
 lib/coq/lib/canary.cmi
 lib/coq/lib/clib.a
 lib/coq/lib/clib.cma
@@ -160,7 +184,6 @@ lib/coq/lib/control.cmi
 lib/coq/lib/deque.cmi
 lib/coq/lib/dyn.cmi
 lib/coq/lib/envars.cmi
-lib/coq/lib/errors.cmi
 lib/coq/lib/exninfo.cmi
 lib/coq/lib/explore.cmi
 lib/coq/lib/feedback.cmi
@@ -178,6 +201,7 @@ lib/coq/lib/lib.a
 lib/coq/lib/lib.cma
 lib/coq/lib/lib.cmxa
 lib/coq/lib/loc.cmi
+lib/coq/lib/minisys.cmi
 lib/coq/lib/monad.cmi
 lib/coq/lib/option.cmi
 lib/coq/lib/pp.cmi
@@ -189,7 +213,6 @@ lib/coq/lib/remoteCounter.cmi
 lib/coq/lib/richpp.cmi
 lib/coq/lib/rtree.cmi
 lib/coq/lib/segmenttree.cmi
-lib/coq/lib/serialize.cmi
 lib/coq/lib/spawn.cmi
 lib/coq/lib/stateid.cmi
 lib/coq/lib/store.cmi
@@ -201,9 +224,6 @@ lib/coq/lib/unicodetable.cmi
 lib/coq/lib/unionfind.cmi
 lib/coq/lib/util.cmi
 lib/coq/lib/xml_datatype.cmi
-lib/coq/lib/xml_lexer.cmi
-lib/coq/lib/xml_parser.cmi
-lib/coq/lib/xml_printer.cmi
 lib/coq/libcoqrun.a
 lib/coq/library/declare.cmi
 lib/coq/library/declaremods.cmi
@@ -229,11 +249,36 @@ lib/coq/library/nametab.cmi
 lib/coq/library/states.cmi
 lib/coq/library/summary.cmi
 lib/coq/library/universes.cmi
+lib/coq/ltac/coretactics.cmi
+lib/coq/ltac/evar_tactics.cmi
+lib/coq/ltac/extraargs.cmi
+lib/coq/ltac/extratactics.cmi
+lib/coq/ltac/g_auto.cmi
+lib/coq/ltac/g_class.cmi
+lib/coq/ltac/g_eqdecide.cmi
+lib/coq/ltac/g_ltac.cmi
+lib/coq/ltac/g_obligations.cmi
+lib/coq/ltac/g_rewrite.cmi
+${PLIST.ocaml-opt}lib/coq/ltac/ltac.a
+lib/coq/ltac/ltac.cma
+${PLIST.ocaml-opt}lib/coq/ltac/ltac.cmxa
+lib/coq/ltac/profile_ltac.cmi
+lib/coq/ltac/profile_ltac_tactics.cmi
+lib/coq/ltac/rewrite.cmi
+lib/coq/ltac/taccoerce.cmi
+lib/coq/ltac/tacentries.cmi
+lib/coq/ltac/tacenv.cmi
+lib/coq/ltac/tacintern.cmi
+lib/coq/ltac/tacinterp.cmi
+lib/coq/ltac/tacsubst.cmi
+lib/coq/ltac/tactic_debug.cmi
+lib/coq/ltac/tactic_option.cmi
+lib/coq/ltac/tauto.cmi
+lib/coq/parsing/cLexer.cmi
 lib/coq/parsing/compat.cmi
 lib/coq/parsing/egramcoq.cmi
 lib/coq/parsing/egramml.cmi
 lib/coq/parsing/g_constr.cmi
-lib/coq/parsing/g_ltac.cmi
 lib/coq/parsing/g_prim.cmi
 lib/coq/parsing/g_proofs.cmi
 lib/coq/parsing/g_tactic.cmi
@@ -241,7 +286,6 @@ lib/coq/parsing/g_vernac.cmi
 lib/coq/parsing/highparsing.a
 lib/coq/parsing/highparsing.cma
 lib/coq/parsing/highparsing.cmxa
-lib/coq/parsing/lexer.cmi
 lib/coq/parsing/parsing.a
 lib/coq/parsing/parsing.cma
 lib/coq/parsing/parsing.cmxa
@@ -268,26 +312,22 @@ lib/coq/plugins/btauto/Btauto.vo
 lib/coq/plugins/btauto/Reflect.glob
 lib/coq/plugins/btauto/Reflect.v
 lib/coq/plugins/btauto/Reflect.vo
-lib/coq/plugins/btauto/btauto_plugin.cma
+lib/coq/plugins/btauto/btauto_plugin.cmi
+lib/coq/plugins/btauto/btauto_plugin.cmo
 lib/coq/plugins/btauto/btauto_plugin.cmxs
-lib/coq/plugins/btauto/btauto_plugin_mod.cmi
-lib/coq/plugins/btauto/g_btauto.cmi
-lib/coq/plugins/btauto/refl_btauto.cmi
-lib/coq/plugins/cc/cc_plugin.cma
+lib/coq/plugins/cc/cc_plugin.cmi
+lib/coq/plugins/cc/cc_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/cc/cc_plugin.cmxs
-lib/coq/plugins/cc/cc_plugin_mod.cmi
 lib/coq/plugins/cc/ccalgo.cmi
 lib/coq/plugins/cc/ccproof.cmi
 lib/coq/plugins/cc/cctac.cmi
-lib/coq/plugins/cc/g_congruence.cmi
 lib/coq/plugins/decl_mode/decl_expr.cmi
 lib/coq/plugins/decl_mode/decl_interp.cmi
 lib/coq/plugins/decl_mode/decl_mode.cmi
-lib/coq/plugins/decl_mode/decl_mode_plugin.cma
+lib/coq/plugins/decl_mode/decl_mode_plugin.cmi
+lib/coq/plugins/decl_mode/decl_mode_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
-lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi
 lib/coq/plugins/decl_mode/decl_proof_instr.cmi
-lib/coq/plugins/decl_mode/g_decl_mode.cmi
 lib/coq/plugins/decl_mode/ppdecl_proof.cmi
 lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmx
@@ -297,9 +337,9 @@ lib/coq/plugins/derive/Derive.glob
 lib/coq/plugins/derive/Derive.v
 lib/coq/plugins/derive/Derive.vo
 lib/coq/plugins/derive/derive.cmi
-lib/coq/plugins/derive/derive_plugin.cma
+lib/coq/plugins/derive/derive_plugin.cmi
+lib/coq/plugins/derive/derive_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/derive/derive_plugin.cmxs
-lib/coq/plugins/derive/g_derive.cmi
 lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmx
 ${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmxs
@@ -415,10 +455,9 @@ lib/coq/plugins/extraction/ExtrOcamlZInt.vo
 lib/coq/plugins/extraction/common.cmi
 lib/coq/plugins/extraction/extract_env.cmi
 lib/coq/plugins/extraction/extraction.cmi
-lib/coq/plugins/extraction/extraction_plugin.cma
+lib/coq/plugins/extraction/extraction_plugin.cmi
+lib/coq/plugins/extraction/extraction_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/extraction/extraction_plugin.cmxs
-lib/coq/plugins/extraction/extraction_plugin_mod.cmi
-lib/coq/plugins/extraction/g_extraction.cmi
 lib/coq/plugins/extraction/haskell.cmi
 lib/coq/plugins/extraction/json.cmi
 lib/coq/plugins/extraction/miniml.cmi
@@ -428,11 +467,10 @@ lib/coq/plugins/extraction/ocaml.cmi
 lib/coq/plugins/extraction/scheme.cmi
 lib/coq/plugins/extraction/table.cmi
 lib/coq/plugins/firstorder/formula.cmi
-lib/coq/plugins/firstorder/g_ground.cmi
 lib/coq/plugins/firstorder/ground.cmi
-lib/coq/plugins/firstorder/ground_plugin.cma
+lib/coq/plugins/firstorder/ground_plugin.cmi
+lib/coq/plugins/firstorder/ground_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/firstorder/ground_plugin.cmxs
-lib/coq/plugins/firstorder/ground_plugin_mod.cmi
 lib/coq/plugins/firstorder/instances.cmi
 lib/coq/plugins/firstorder/rules.cmi
 lib/coq/plugins/firstorder/sequent.cmi
@@ -451,12 +489,9 @@ lib/coq/plugins/fourier/Fourier.vo
 lib/coq/plugins/fourier/Fourier_util.glob
 lib/coq/plugins/fourier/Fourier_util.v
 lib/coq/plugins/fourier/Fourier_util.vo
-lib/coq/plugins/fourier/fourier.cmi
-lib/coq/plugins/fourier/fourierR.cmi
-lib/coq/plugins/fourier/fourier_plugin.cma
+lib/coq/plugins/fourier/fourier_plugin.cmi
+lib/coq/plugins/fourier/fourier_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/fourier/fourier_plugin.cmxs
-lib/coq/plugins/fourier/fourier_plugin_mod.cmi
-lib/coq/plugins/fourier/g_fourier.cmi
 lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmx
 ${PLIST.natdynlink}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmxs
@@ -466,17 +501,14 @@ lib/coq/plugins/funind/Recdef.v
 lib/coq/plugins/funind/Recdef.vo
 lib/coq/plugins/funind/functional_principles_proofs.cmi
 lib/coq/plugins/funind/functional_principles_types.cmi
-lib/coq/plugins/funind/g_indfun.cmi
 lib/coq/plugins/funind/glob_term_to_relation.cmi
 lib/coq/plugins/funind/glob_termops.cmi
 lib/coq/plugins/funind/indfun.cmi
 lib/coq/plugins/funind/indfun_common.cmi
-lib/coq/plugins/funind/invfun.cmi
-lib/coq/plugins/funind/merge.cmi
 lib/coq/plugins/funind/recdef.cmi
-lib/coq/plugins/funind/recdef_plugin.cma
+lib/coq/plugins/funind/recdef_plugin.cmi
+lib/coq/plugins/funind/recdef_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/funind/recdef_plugin.cmxs
-lib/coq/plugins/funind/recdef_plugin_mod.cmi
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmx
 ${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmxs
@@ -489,6 +521,14 @@ lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmx
 ${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.o
+lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmx
+${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.o
+lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmx
+${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.o
 lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmx
 ${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmxs
@@ -538,6 +578,12 @@ lib/coq/plugins/micromega/EnvRing.vo
 lib/coq/plugins/micromega/Lia.glob
 lib/coq/plugins/micromega/Lia.v
 lib/coq/plugins/micromega/Lia.vo
+lib/coq/plugins/micromega/Lqa.glob
+lib/coq/plugins/micromega/Lqa.v
+lib/coq/plugins/micromega/Lqa.vo
+lib/coq/plugins/micromega/Lra.glob
+lib/coq/plugins/micromega/Lra.v
+lib/coq/plugins/micromega/Lra.vo
 lib/coq/plugins/micromega/OrderedRing.glob
 lib/coq/plugins/micromega/OrderedRing.v
 lib/coq/plugins/micromega/OrderedRing.vo
@@ -568,20 +614,12 @@ lib/coq/plugins/micromega/ZCoeff.vo
 lib/coq/plugins/micromega/ZMicromega.glob
 lib/coq/plugins/micromega/ZMicromega.v
 lib/coq/plugins/micromega/ZMicromega.vo
-lib/coq/plugins/micromega/certificate.cmi
-lib/coq/plugins/micromega/coq_micromega.cmi
 lib/coq/plugins/micromega/csdpcert
-lib/coq/plugins/micromega/g_micromega.cmi
-lib/coq/plugins/micromega/mfourier.cmi
 lib/coq/plugins/micromega/micromega.cmi
-lib/coq/plugins/micromega/micromega_plugin.cma
+lib/coq/plugins/micromega/micromega_plugin.cmi
+lib/coq/plugins/micromega/micromega_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/micromega/micromega_plugin.cmxs
-lib/coq/plugins/micromega/micromega_plugin_mod.cmi
-lib/coq/plugins/micromega/mutils.cmi
-lib/coq/plugins/micromega/persistent_cache.cmi
-lib/coq/plugins/micromega/polynomial.cmi
 lib/coq/plugins/micromega/sos.cmi
-lib/coq/plugins/micromega/sos_types.cmi
 lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmx
 ${PLIST.natdynlink}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmxs
@@ -591,9 +629,9 @@ lib/coq/plugins/nsatz/Nsatz.v
 lib/coq/plugins/nsatz/Nsatz.vo
 lib/coq/plugins/nsatz/ideal.cmi
 lib/coq/plugins/nsatz/nsatz.cmi
-lib/coq/plugins/nsatz/nsatz_plugin.cma
+lib/coq/plugins/nsatz/nsatz_plugin.cmi
+lib/coq/plugins/nsatz/nsatz_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/nsatz/nsatz_plugin.cmxs
-lib/coq/plugins/nsatz/nsatz_plugin_mod.cmi
 lib/coq/plugins/nsatz/polynom.cmi
 lib/coq/plugins/nsatz/utile.cmi
 lib/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmi
@@ -631,12 +669,9 @@ lib/coq/plugins/omega/OmegaTactic.vo
 lib/coq/plugins/omega/PreOmega.glob
 lib/coq/plugins/omega/PreOmega.v
 lib/coq/plugins/omega/PreOmega.vo
-lib/coq/plugins/omega/coq_omega.cmi
-lib/coq/plugins/omega/g_omega.cmi
-lib/coq/plugins/omega/omega.cmi
-lib/coq/plugins/omega/omega_plugin.cma
+lib/coq/plugins/omega/omega_plugin.cmi
+lib/coq/plugins/omega/omega_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/omega/omega_plugin.cmxs
-lib/coq/plugins/omega/omega_plugin_mod.cmi
 lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmx
 ${PLIST.natdynlink}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmxs
@@ -644,11 +679,9 @@ ${PLIST.ocaml-opt}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.o
 lib/coq/plugins/quote/Quote.glob
 lib/coq/plugins/quote/Quote.v
 lib/coq/plugins/quote/Quote.vo
-lib/coq/plugins/quote/g_quote.cmi
-lib/coq/plugins/quote/quote.cmi
-lib/coq/plugins/quote/quote_plugin.cma
+lib/coq/plugins/quote/quote_plugin.cmi
+lib/coq/plugins/quote/quote_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/quote/quote_plugin.cmxs
-lib/coq/plugins/quote/quote_plugin_mod.cmi
 lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmx
 ${PLIST.natdynlink}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmxs
@@ -664,11 +697,9 @@ lib/coq/plugins/romega/ReflOmegaCore.glob
 lib/coq/plugins/romega/ReflOmegaCore.v
 lib/coq/plugins/romega/ReflOmegaCore.vo
 lib/coq/plugins/romega/const_omega.cmi
-lib/coq/plugins/romega/g_romega.cmi
-lib/coq/plugins/romega/refl_omega.cmi
-lib/coq/plugins/romega/romega_plugin.cma
+lib/coq/plugins/romega/romega_plugin.cmi
+lib/coq/plugins/romega/romega_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/romega/romega_plugin.cmxs
-lib/coq/plugins/romega/romega_plugin_mod.cmi
 lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmx
 ${PLIST.natdynlink}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmxs
@@ -683,12 +714,11 @@ lib/coq/plugins/rtauto/Bintree.vo
 lib/coq/plugins/rtauto/Rtauto.glob
 lib/coq/plugins/rtauto/Rtauto.v
 lib/coq/plugins/rtauto/Rtauto.vo
-lib/coq/plugins/rtauto/g_rtauto.cmi
 lib/coq/plugins/rtauto/proof_search.cmi
 lib/coq/plugins/rtauto/refl_tauto.cmi
-lib/coq/plugins/rtauto/rtauto_plugin.cma
+lib/coq/plugins/rtauto/rtauto_plugin.cmi
+lib/coq/plugins/rtauto/rtauto_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/rtauto/rtauto_plugin.cmxs
-lib/coq/plugins/rtauto/rtauto_plugin_mod.cmi
 lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmx
 ${PLIST.natdynlink}lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmxs
@@ -858,33 +888,39 @@ lib/coq/plugins/setoid_ring/ZArithRing.glob
 lib/coq/plugins/setoid_ring/ZArithRing.v
 lib/coq/plugins/setoid_ring/ZArithRing.vo
 lib/coq/plugins/setoid_ring/newring.cmi
-lib/coq/plugins/setoid_ring/newring_plugin.cma
+lib/coq/plugins/setoid_ring/newring_ast.cmi
+lib/coq/plugins/setoid_ring/newring_plugin.cmi
+lib/coq/plugins/setoid_ring/newring_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/setoid_ring/newring_plugin.cmxs
-lib/coq/plugins/setoid_ring/newring_plugin_mod.cmi
-lib/coq/plugins/syntax/ascii_syntax.cmi
-lib/coq/plugins/syntax/ascii_syntax_plugin.cma
+lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
+${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmx
+${PLIST.natdynlink}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmxs
+${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.o
+lib/coq/plugins/ssrmatching/ssrmatching.cmi
+lib/coq/plugins/ssrmatching/ssrmatching.glob
+lib/coq/plugins/ssrmatching/ssrmatching.v
+lib/coq/plugins/ssrmatching/ssrmatching.vo
+lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
+lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmo
+lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmxs
+lib/coq/plugins/syntax/ascii_syntax_plugin.cmi
+lib/coq/plugins/syntax/ascii_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
-lib/coq/plugins/syntax/ascii_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/nat_syntax.cmi
-lib/coq/plugins/syntax/nat_syntax_plugin.cma
+lib/coq/plugins/syntax/nat_syntax_plugin.cmi
+lib/coq/plugins/syntax/nat_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
-lib/coq/plugins/syntax/nat_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/numbers_syntax.cmi
-lib/coq/plugins/syntax/numbers_syntax_plugin.cma
+lib/coq/plugins/syntax/numbers_syntax_plugin.cmi
+lib/coq/plugins/syntax/numbers_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs
-lib/coq/plugins/syntax/numbers_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/r_syntax.cmi
-lib/coq/plugins/syntax/r_syntax_plugin.cma
+lib/coq/plugins/syntax/r_syntax_plugin.cmi
+lib/coq/plugins/syntax/r_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/r_syntax_plugin.cmxs
-lib/coq/plugins/syntax/r_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/string_syntax.cmi
-lib/coq/plugins/syntax/string_syntax_plugin.cma
+lib/coq/plugins/syntax/string_syntax_plugin.cmi
+lib/coq/plugins/syntax/string_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/string_syntax_plugin.cmxs
-lib/coq/plugins/syntax/string_syntax_plugin_mod.cmi
-lib/coq/plugins/syntax/z_syntax.cmi
-lib/coq/plugins/syntax/z_syntax_plugin.cma
+lib/coq/plugins/syntax/z_syntax_plugin.cmi
+lib/coq/plugins/syntax/z_syntax_plugin.cmo
 ${PLIST.natdynlink}lib/coq/plugins/syntax/z_syntax_plugin.cmxs
-lib/coq/plugins/syntax/z_syntax_plugin_mod.cmi
 lib/coq/pretyping/arguments_renaming.cmi
 lib/coq/pretyping/cases.cmi
 lib/coq/pretyping/cbv.cmi
@@ -893,16 +929,14 @@ lib/coq/pretyping/coercion.cmi
 lib/coq/pretyping/constr_matching.cmi
 lib/coq/pretyping/detyping.cmi
 lib/coq/pretyping/evarconv.cmi
+lib/coq/pretyping/evardefine.cmi
 lib/coq/pretyping/evarsolve.cmi
-lib/coq/pretyping/evarutil.cmi
-lib/coq/pretyping/evd.cmi
 lib/coq/pretyping/find_subterm.cmi
 lib/coq/pretyping/glob_ops.cmi
 lib/coq/pretyping/indrec.cmi
 lib/coq/pretyping/inductiveops.cmi
 lib/coq/pretyping/locusops.cmi
 lib/coq/pretyping/miscops.cmi
-lib/coq/pretyping/namegen.cmi
 lib/coq/pretyping/nativenorm.cmi
 lib/coq/pretyping/patternops.cmi
 lib/coq/pretyping/pretype_errors.cmi
@@ -916,7 +950,6 @@ lib/coq/pretyping/redops.cmi
 lib/coq/pretyping/reductionops.cmi
 lib/coq/pretyping/retyping.cmi
 lib/coq/pretyping/tacred.cmi
-lib/coq/pretyping/termops.cmi
 lib/coq/pretyping/typeclasses.cmi
 lib/coq/pretyping/typeclasses_errors.cmi
 lib/coq/pretyping/typing.cmi
@@ -939,13 +972,11 @@ lib/coq/printing/printing.cma
 ${PLIST.ocaml-opt}lib/coq/printing/printing.cmxa
 lib/coq/printing/printmod.cmi
 lib/coq/printing/printmodsig.cmi
-lib/coq/printing/richprinter.cmi
 lib/coq/proofs/clenv.cmi
 lib/coq/proofs/clenvtac.cmi
 lib/coq/proofs/evar_refiner.cmi
 lib/coq/proofs/goal.cmi
 lib/coq/proofs/logic.cmi
-lib/coq/proofs/logic_monad.cmi
 lib/coq/proofs/pfedit.cmi
 lib/coq/proofs/proof.cmi
 lib/coq/proofs/proof_global.cmi
@@ -954,12 +985,10 @@ lib/coq/proofs/proof_using.cmi
 ${PLIST.ocaml-opt}lib/coq/proofs/proofs.a
 lib/coq/proofs/proofs.cma
 ${PLIST.ocaml-opt}lib/coq/proofs/proofs.cmxa
-lib/coq/proofs/proofview.cmi
-lib/coq/proofs/proofview_monad.cmi
 lib/coq/proofs/redexpr.cmi
+lib/coq/proofs/refine.cmi
 lib/coq/proofs/refiner.cmi
 lib/coq/proofs/tacmach.cmi
-lib/coq/proofs/tactic_debug.cmi
 lib/coq/stm/asyncTaskQueue.cmi
 lib/coq/stm/coqworkmgrApi.cmi
 lib/coq/stm/dag.cmi
@@ -969,8 +998,8 @@ ${PLIST.ocaml-opt}lib/coq/stm/stm.a
 lib/coq/stm/stm.cma
 lib/coq/stm/stm.cmi
 ${PLIST.ocaml-opt}lib/coq/stm/stm.cmxa
+lib/coq/stm/proofBlockDelimiter.cmi
 lib/coq/stm/tQueue.cmi
-lib/coq/stm/texmacspp.cmi
 lib/coq/stm/vcs.cmi
 lib/coq/stm/vernac_classifier.cmi
 lib/coq/stm/vio_checking.cmi
@@ -980,7 +1009,6 @@ lib/coq/tactics/autorewrite.cmi
 lib/coq/tactics/btermdn.cmi
 lib/coq/tactics/class_tactics.cmi
 lib/coq/tactics/contradiction.cmi
-lib/coq/tactics/coretactics.cmi
 lib/coq/tactics/dn.cmi
 lib/coq/tactics/dnet.cmi
 lib/coq/tactics/eauto.cmi
@@ -989,35 +1017,16 @@ lib/coq/tactics/elimschemes.cmi
 lib/coq/tactics/eqdecide.cmi
 lib/coq/tactics/eqschemes.cmi
 lib/coq/tactics/equality.cmi
-lib/coq/tactics/evar_tactics.cmi
-lib/coq/tactics/extraargs.cmi
-lib/coq/tactics/extratactics.cmi
-lib/coq/tactics/ftactic.cmi
-lib/coq/tactics/g_class.cmi
-lib/coq/tactics/g_eqdecide.cmi
-lib/coq/tactics/g_rewrite.cmi
-lib/coq/tactics/geninterp.cmi
-${PLIST.ocaml-opt}lib/coq/tactics/hightactics.a
-lib/coq/tactics/hightactics.cma
-${PLIST.ocaml-opt}lib/coq/tactics/hightactics.cmxa
 lib/coq/tactics/hints.cmi
 lib/coq/tactics/hipattern.cmi
 lib/coq/tactics/inv.cmi
 lib/coq/tactics/leminv.cmi
-lib/coq/tactics/rewrite.cmi
-lib/coq/tactics/taccoerce.cmi
-lib/coq/tactics/tacenv.cmi
-lib/coq/tactics/tacintern.cmi
-lib/coq/tactics/tacinterp.cmi
-lib/coq/tactics/tacsubst.cmi
 lib/coq/tactics/tactic_matching.cmi
-lib/coq/tactics/tactic_option.cmi
 lib/coq/tactics/tacticals.cmi
 ${PLIST.ocaml-opt}lib/coq/tactics/tactics.a
 lib/coq/tactics/tactics.cma
 lib/coq/tactics/tactics.cmi
 ${PLIST.ocaml-opt}lib/coq/tactics/tactics.cmxa
-lib/coq/tactics/tauto.cmi
 lib/coq/tactics/term_dnet.cmi
 lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmi
 ${PLIST.ocaml-opt}lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmx
@@ -1327,6 +1336,7 @@ lib/coq/theories/Classes/SetoidDec.vo
 lib/coq/theories/Classes/SetoidTactics.glob
 lib/coq/theories/Classes/SetoidTactics.v
 lib/coq/theories/Classes/SetoidTactics.vo
+lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmi
 lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmi
 ${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmx
 ${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs
@@ -1339,6 +1349,9 @@ lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmi
 ${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmx
 ${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmxs
 ${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.o
+${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmx
+${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmxs
+${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.o
 lib/coq/theories/Compat/AdmitAxiom.glob
 lib/coq/theories/Compat/AdmitAxiom.v
 lib/coq/theories/Compat/AdmitAxiom.glob
@@ -1354,6 +1367,9 @@ lib/coq/theories/Compat/Coq85.v
 lib/coq/theories/Compat/Coq85.glob
 lib/coq/theories/Compat/Coq85.v
 lib/coq/theories/Compat/Coq85.vo
+lib/coq/theories/Compat/Coq86.glob
+lib/coq/theories/Compat/Coq86.v
+lib/coq/theories/Compat/Coq86.vo
 lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi
 ${PLIST.ocaml-opt}lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmx
 ${PLIST.natdynlink}lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmxs
@@ -1537,6 +1553,10 @@ lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmi
 ${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmx
 ${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmxs
 ${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.o
+lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmi
+${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmx
+${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmxs
+${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.o
 lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmi
 ${PLIST.ocaml-opt}lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmx
 ${PLIST.natdynlink}lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmxs
@@ -1568,6 +1588,9 @@ lib/coq/theories/Init/Specif.vo
 lib/coq/theories/Init/Tactics.glob
 lib/coq/theories/Init/Tactics.v
 lib/coq/theories/Init/Tactics.vo
+lib/coq/theories/Init/Tauto.glob
+lib/coq/theories/Init/Tauto.v
+lib/coq/theories/Init/Tauto.vo
 lib/coq/theories/Init/Wf.glob
 lib/coq/theories/Init/Wf.v
 lib/coq/theories/Init/Wf.vo
@@ -2749,6 +2772,10 @@ lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmi
 ${PLIST.ocaml-opt}lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmx
 ${PLIST.natdynlink}lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmxs
 ${PLIST.ocaml-opt}lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.o
+lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmi
+${PLIST.ocaml-opt}lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmx
+${PLIST.natdynlink}lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmxs
+${PLIST.ocaml-opt}lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.o
 lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmi
 ${PLIST.ocaml-opt}lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmx
 ${PLIST.natdynlink}lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmxs
@@ -2793,6 +2820,9 @@ lib/coq/theories/QArith/QOrderedType.vo
 lib/coq/theories/QArith/Qabs.glob
 lib/coq/theories/QArith/Qabs.v
 lib/coq/theories/QArith/Qabs.vo
+lib/coq/theories/QArith/Qcabs.glob
+lib/coq/theories/QArith/Qcabs.v
+lib/coq/theories/QArith/Qcabs.vo
 lib/coq/theories/QArith/Qcanon.glob
 lib/coq/theories/QArith/Qcanon.v
 lib/coq/theories/QArith/Qcanon.vo
@@ -3944,12 +3974,10 @@ lib/coq/theories/ZArith/Zwf.vo
 lib/coq/theories/ZArith/auxiliary.glob
 lib/coq/theories/ZArith/auxiliary.v
 lib/coq/theories/ZArith/auxiliary.vo
-lib/coq/tools/compat5.cmo
 lib/coq/tools/coqdoc/coqdoc.css
 lib/coq/tools/coqdoc/coqdoc.sty
 lib/coq/toplevel/assumptions.cmi
 lib/coq/toplevel/auto_ind_decl.cmi
-lib/coq/toplevel/cerrors.cmi
 lib/coq/toplevel/class.cmi
 lib/coq/toplevel/classes.cmi
 lib/coq/toplevel/command.cmi
@@ -3957,7 +3985,7 @@ lib/coq/toplevel/coqinit.cmi
 lib/coq/toplevel/coqloop.cmi
 lib/coq/toplevel/coqtop.cmi
 lib/coq/toplevel/discharge.cmi
-lib/coq/toplevel/g_obligations.cmi
+lib/coq/toplevel/explainErr.cmi
 lib/coq/toplevel/himsg.cmi
 lib/coq/toplevel/ind_tables.cmi
 lib/coq/toplevel/indschemes.cmi
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index b2e9ac07091..4b3bfc77824 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,9 +1,8 @@
-$NetBSD: distinfo,v 1.25 2016/07/02 10:17:18 jaapb Exp $
+$NetBSD: distinfo,v 1.26 2016/12/30 13:23:06 jaapb Exp $
 
-SHA1 (coq-8.5pl1.tar.gz) = 92722ffc2be6948e0074b211bb556ad4b911ebd6
-RMD160 (coq-8.5pl1.tar.gz) = 04c540ab1033fd6b0e4c121b73ed56557708e7a5
-SHA512 (coq-8.5pl1.tar.gz) = c9a5bba1abc3b2216cb43595230387751277412988b44af1555ffccdc109a9eef69422867e0062d92dfc73ffcbbe24f53ff583224c28cae3f9bda1ae21dd547b
-Size (coq-8.5pl1.tar.gz) = 5366774 bytes
-SHA1 (patch-Makefile.build) = 1b711ef9490a07c9d02b5a8ca9a38c252e322b4f
-SHA1 (patch-Makefile.common) = f53dd334d3e14a0e0c3ef91bac9a6c1745cbb591
-SHA1 (patch-configure.ml) = 6e2f44091216348a12131592bf29f0f7fd93a4fe
+SHA1 (coq-8.6.tar.gz) = 617a6f86d09dde0e409f3fa22268daf7be3f5bba
+RMD160 (coq-8.6.tar.gz) = 3d5e539c40732620e65f28988b118d2e0d663aa5
+SHA512 (coq-8.6.tar.gz) = 9f5f4913fda8cf83683fec9398b42d4567207c3d4b52b4638d5e09a24ed25a43905fb57a9fac1bb9f9d681bd47f3560e1da74e79348b3a3fd93e2e8c686cebae
+Size (coq-8.6.tar.gz) = 5538848 bytes
+SHA1 (patch-Makefile.common) = 79b02edff66ddcfb267816b0031c724620e67a13
+SHA1 (patch-configure.ml) = 8e48a65709234281e3898ebae9041dfc04c7fe7b
diff --git a/lang/coq/patches/patch-Makefile.build b/lang/coq/patches/patch-Makefile.build
deleted file mode 100644
index f382a7e2be9..00000000000
--- a/lang/coq/patches/patch-Makefile.build
+++ /dev/null
@@ -1,23 +0,0 @@
-$NetBSD: patch-Makefile.build,v 1.3 2016/02/06 16:08:36 jaapb Exp $
-
-Install in the right directory
---- Makefile.build.orig	2015-12-16 23:44:44.000000000 +0000
-+++ Makefile.build
-@@ -712,7 +712,7 @@ install-doc-no:
- ifdef COQINSTALLPREFIX
- FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
- FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
--FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-+FULLCONFIGDIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)/examples
- FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
- FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
- FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-@@ -721,7 +721,7 @@ FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQI
- else
- FULLBINDIR=$(BINDIR)
- FULLCOQLIB=$(COQLIBINSTALL)
--FULLCONFIGDIR=$(CONFIGDIR)
-+FULLCONFIGDIR=$(DATADIR)/examples
- FULLDATADIR=$(DATADIR)
- FULLMANDIR=$(MANDIR)
- FULLEMACSLIB=$(EMACSLIB)
diff --git a/lang/coq/patches/patch-Makefile.common b/lang/coq/patches/patch-Makefile.common
index 19806bbbaec..11f2babbc12 100644
--- a/lang/coq/patches/patch-Makefile.common
+++ b/lang/coq/patches/patch-Makefile.common
@@ -1,8 +1,7 @@
-$NetBSD: patch-Makefile.common,v 1.2 2016/07/02 10:17:18 jaapb Exp $
+$NetBSD: patch-Makefile.common,v 1.3 2016/12/30 13:23:06 jaapb Exp $
 
 Use BSD_INSTALL_*
-Compile with OCaml 4.03
---- Makefile.common.orig	2016-04-11 13:12:51.000000000 +0000
+--- Makefile.common.orig	2016-10-25 20:17:16.000000000 +0000
 +++ Makefile.common
 @@ -35,7 +35,7 @@ else
  endif
@@ -13,12 +12,3 @@ Compile with OCaml 4.03
  INSTALLSH:=./install.sh
  MKDIR:=install -d
  
-@@ -231,7 +231,7 @@ endif
- LINKCMO:=$(CORECMA) $(STATICPLUGINS)
- LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
- 
--IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo
-+IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo
- IDECMA:=ide/ide.cma
- IDETOPLOOPCMA=ide/coqidetop.cma
- 
diff --git a/lang/coq/patches/patch-configure.ml b/lang/coq/patches/patch-configure.ml
index 6eabbcfa6fd..efffa43af14 100644
--- a/lang/coq/patches/patch-configure.ml
+++ b/lang/coq/patches/patch-configure.ml
@@ -1,14 +1,14 @@
-$NetBSD: patch-configure.ml,v 1.1 2016/02/06 16:08:36 jaapb Exp $
+$NetBSD: patch-configure.ml,v 1.2 2016/12/30 13:23:06 jaapb Exp $
 
 NetBSD uses md5sum too
---- configure.ml.orig	2015-12-16 23:44:44.000000000 +0000
+--- configure.ml.orig	2016-10-25 20:17:16.000000000 +0000
 +++ configure.ml
-@@ -843,7 +843,7 @@ let strip =
+@@ -827,7 +827,7 @@ let strip =
  (** * md5sum command *)
  
  let md5sum =
--  if arch = "Darwin" then "md5 -q" else "md5sum"
-+  if arch = "Darwin" || arch = "NetBSD" then "md5 -q" else "md5sum"
+-  if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"]
++  if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"; "NetBSD"]
+   then "md5 -q" else "md5sum"
  
  
- (** * Documentation : do we have latex, hevea, ... *)
author	jaapb <jaapb>	2016-12-30 13:23:06 +0000
committer	jaapb <jaapb>	2016-12-30 13:23:06 +0000
commit	40ffa23afb27611843446f19e713dc0bf76d9020 (patch)
tree	6b0f4f66439c2e7cb191a3ace939fd685c091ef1 /lang
parent	441c004edc347960b94a297f8de9854d7a308f49 (diff)
download	pkgsrc-40ffa23afb27611843446f19e713dc0bf76d9020.tar.gz