[pkgsrc/trunk]: pkgsrc/lang/coq Updated coq to latest version, 8.6. Changes i...

[jaapb <jaapb%pkgsrc.org@localhost>]

details:   https://anonhg.NetBSD.org/pkgsrc/rev/ab02022cd4ae
branches:  trunk
changeset: 356402:ab02022cd4ae
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Fri Dec 30 13:23:06 2016 +0000

description:
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.

diffstat:

 lang/coq/Makefile                      |    6 +-
 lang/coq/PLIST                         |  266 ++++++++++++++++++--------------
 lang/coq/distinfo                      |   15 +-
 lang/coq/patches/patch-Makefile.build  |   23 --
 lang/coq/patches/patch-Makefile.common |   14 +-
 lang/coq/patches/patch-configure.ml    |   12 +-
 6 files changed, 164 insertions(+), 172 deletions(-)

diffs (truncated from 780 to 300 lines):

diff -r ec533074c31b -r ab02022cd4ae lang/coq/Makefile
--- a/lang/coq/Makefile Fri Dec 30 12:54:20 2016 +0000
+++ b/lang/coq/Makefile Fri Dec 30 13:23:06 2016 +0000
@@ -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_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 -r ec533074c31b -r ab02022cd4ae lang/coq/PLIST
--- a/lang/coq/PLIST    Fri Dec 30 12:54:20 2016 +0000
+++ b/lang/coq/PLIST    Fri Dec 30 13:23:06 2016 +0000
@@ -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/coqwc
 bin/coqworkmgr
 bin/gallina
+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/dllcoqrun.so
 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/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_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/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_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/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/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/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.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/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/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/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/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/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.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/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/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_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.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