[pkgsrc/trunk]: pkgsrc/lang/coq Update lang/coq to 8.12.2.

To: pkgsrc-changes-hg%NetBSD.org@localhost
Subject: [pkgsrc/trunk]: pkgsrc/lang/coq Update lang/coq to 8.12.2.
From: dholland <dholland%pkgsrc.org@localhost>
Date: Tue, 09 Feb 2021 23:34:47 +0000
details:   https://anonhg.NetBSD.org/pkgsrc/rev/8e3527ac295a
branches:  trunk
changeset: 446498:8e3527ac295a
user:      dholland <dholland%pkgsrc.org@localhost>
date:      Tue Feb 09 22:37:43 2021 +0000

description:
Update lang/coq to 8.12.2.

Fixes build with current ocaml.

Note: this update includes the import semantics fixes from 8.11 that
break a lot of developments.

pkgsrc change: docs build now works.


Summary of changes in 8.12:

Coq version 8.12 integrates many usability improvements, in particular
with respect to notations, scopes and implicit arguments, along with
many bug fixes and major improvements to the reference manual. The
main changes include:

    New binder notation for non-maximal implicit arguments using [ ]
    allowing to set and see the implicit status of arguments
   immediately.

    New notation Inductive I A | x : s := ... to distinguish the
    uniform from the non-uniform parameters in inductive definitions.

    More robust and expressive treatment of implicit inductive
    parameters in inductive declarations.

    Improvements in the treatment of implicit arguments and partially
    applied constants in notations, parsing of hexadecimal number
    notation and better handling of scopes and coercions for printing.

    A correct and efficient coercion coherence checking algorithm,
    avoiding spurious or duplicate warnings.

    An improved Search command which accepts complex queries. Note
    that this takes precedence over the now deprecated ssreflect
    search.

    Many additions and improvements of the standard library.

    Improvements to the reference manual include a more logical
    organization of chapters along with updated syntax descriptions
    that match Coq's grammar in most but not all chapters.

Additionally, the omega tactic is deprecated in this version of Coq,
and we recommend users to switch to lia in new proof scripts (see also
the warning message in the corresponding chapter).

Summary of changes in 8.11:

The main changes brought by Coq version 8.11 are:

    Ltac2, a new tactic language for writing more robust larger scale
    tactics, with built-in support for datatypes and the multi-goal
    tactic monad.

    Primitive floats are integrated in terms and follow the binary64
    format of the IEEE 754 standard, as specified in the
    Coq.Float.Floats library.

    Cleanups of the section mechanism, delayed proofs and further
    restrictions of template polymorphism to fix soundness issues
    related to universes.

    New unsafe flags to disable locally guard, positivity and universe
    checking. Reliance on these flags is always printed by Print
    Assumptions.

    Fixed bugs of Export and Import that can have a significant impact
    on user developments (common source of incompatibility!).

    New interactive development method based on vos interface files,
    allowing to work on a file without recompiling the proof parts of
    their dependencies.

    New Arguments annotation for bidirectional type inference
    configuration for reference (e.g. constants, inductive)
    applications.

    New refine attribute for Instance can be used instead of the
    removed Refine Instance Mode.

    Generalization of the under and over tactics of SSReflect to
    arbitrary relations.

    Revision of the Coq.Reals library, its axiomatisation and
    instances of the constructive and classical real numbers.

Additionally, while the omega tactic is not yet deprecated in this
version of Coq, it should soon be the case and we already recommend
users to switch to lia in new proof scripts (see also the warning
message in the corresponding chapter).


The full (huge) changelog is here:
https://coq.inria.fr/distrib/V8.12.2/refman/changes.html

diffstat:

 lang/coq/Makefile                      |    11 +-
 lang/coq/PLIST                         |  2656 +++++++++++++++++++++++--------
 lang/coq/distinfo                      |    13 +-
 lang/coq/options.mk                    |    33 +-
 lang/coq/patches/patch-Makefile.common |     6 +-
 lang/coq/patches/patch-Makefile.make   |    15 +
 6 files changed, 2021 insertions(+), 713 deletions(-)

diffs (truncated from 4926 to 300 lines):

diff -r f0b1d7fcca33 -r 8e3527ac295a lang/coq/Makefile
--- a/lang/coq/Makefile Tue Feb 09 22:33:59 2021 +0000
+++ b/lang/coq/Makefile Tue Feb 09 22:37:43 2021 +0000
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.136 2020/11/05 09:08:33 ryoon Exp $
+# $NetBSD: Makefile,v 1.137 2021/02/09 22:37:43 dholland Exp $
 #
 
-DISTNAME=      coq-8.10.2
-PKGREVISION=   6
+DISTNAME=      coq-8.12.2
 CATEGORIES=    lang math
 MASTER_SITES=  ${MASTER_SITE_GITHUB:=coq/}
 GITHUB_TAG=    V${PKGVERSION_NOREV:S/_/+/}
@@ -27,6 +26,12 @@
 
 BUILDLINK_API_DEPENDS.ocaml+=  ocaml>=3.10
 
+# datestamp for reproducible builds (this ends up in compiled proofs)
+# Use the upstream release date plus (arbitrarily) 11 days, the latter
+# being a venture to hopefully avoid accepting compiled proof files from
+# elsewhere that likely are not in fact compatible.
+MAKE_ENV+=             SOURCE_DATE_EPOCH=20201222
+
 .include "../../mk/bsd.prefs.mk"
 .include "../../mk/ocaml.mk"
 
diff -r f0b1d7fcca33 -r 8e3527ac295a lang/coq/PLIST
--- a/lang/coq/PLIST    Tue Feb 09 22:33:59 2021 +0000
+++ b/lang/coq/PLIST    Tue Feb 09 22:37:43 2021 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.30 2020/01/24 15:54:48 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.31 2021/02/09 22:37:43 dholland Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -16,9 +16,9 @@
 bin/coqtop.opt
 bin/coqwc
 bin/coqworkmgr
+bin/ocamllibdep
+bin/votour
 lib/coq/META
-lib/coq/clib/backtrace.cmi
-${PLIST.ocaml-opt}lib/coq/clib/backtrace.cmx
 lib/coq/clib/bigint.cmi
 ${PLIST.ocaml-opt}lib/coq/clib/bigint.cmx
 lib/coq/clib/cArray.cmi
@@ -34,8 +34,6 @@
 lib/coq/clib/cSet.cmi
 ${PLIST.ocaml-opt}lib/coq/clib/cSet.cmx
 lib/coq/clib/cSig.cmi
-lib/coq/clib/cStack.cmi
-${PLIST.ocaml-opt}lib/coq/clib/cStack.cmx
 lib/coq/clib/cString.cmi
 ${PLIST.ocaml-opt}lib/coq/clib/cString.cmx
 lib/coq/clib/cThread.cmi
@@ -94,6 +92,7 @@
 ${PLIST.ocaml-opt}lib/coq/config/coq_config.cmx
 lib/coq/coqpp/coqpp_ast.cmi
 lib/coq/coqpp/coqpp_parse.cmi
+lib/coq/coqpp/coqpp_parser.cmi
 lib/coq/engine/eConstr.cmi
 ${PLIST.ocaml-opt}lib/coq/engine/eConstr.cmx
 ${PLIST.ocaml-opt}lib/coq/engine/engine.a
@@ -157,8 +156,8 @@
 ${PLIST.coqide}lib/coq/ide/document.cmi
 ${PLIST.coqide}lib/coq/ide/fileOps.cmi
 ${PLIST.coqide}lib/coq/ide/gtk_parsing.cmi
-${PLIST.coqide}${PLIST.ocaml-opt}lib/coq/ide/ide.a
-${PLIST.coqide}${PLIST.ocaml-opt}lib/coq/ide/ide.cmxa
+${PLIST.ocaml-opt}${PLIST.coqide}lib/coq/ide/ide.a
+${PLIST.ocaml-opt}${PLIST.coqide}lib/coq/ide/ide.cmxa
 ${PLIST.coqide}lib/coq/ide/ideutils.cmi
 ${PLIST.coqide}lib/coq/ide/microPG.cmi
 ${PLIST.coqide}lib/coq/ide/minilib.cmi
@@ -186,10 +185,10 @@
 ${PLIST.ocaml-opt}lib/coq/interp/constrextern.cmx
 lib/coq/interp/constrintern.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/constrintern.cmx
-lib/coq/interp/declare.cmi
-${PLIST.ocaml-opt}lib/coq/interp/declare.cmx
-lib/coq/interp/discharge.cmi
-${PLIST.ocaml-opt}lib/coq/interp/discharge.cmx
+lib/coq/interp/decls.cmi
+${PLIST.ocaml-opt}lib/coq/interp/decls.cmx
+lib/coq/interp/deprecation.cmi
+${PLIST.ocaml-opt}lib/coq/interp/deprecation.cmx
 lib/coq/interp/dumpglob.cmi
 ${PLIST.ocaml-opt}lib/coq/interp/dumpglob.cmx
 lib/coq/interp/genintern.cmi
@@ -256,12 +255,16 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/esubst.cmx
 lib/coq/kernel/evar.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/evar.cmx
+lib/coq/kernel/float64.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/float64.cmx
 lib/coq/kernel/indTyping.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/indTyping.cmx
 lib/coq/kernel/indtypes.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/indtypes.cmx
 lib/coq/kernel/inductive.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/inductive.cmx
+lib/coq/kernel/inferCumulativity.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/inferCumulativity.cmx
 ${PLIST.ocaml-opt}lib/coq/kernel/kernel.a
 ${PLIST.ocaml-opt}lib/coq/kernel/kernel.cmxa
 lib/coq/kernel/mod_subst.cmi
@@ -290,12 +293,14 @@
 ${PLIST.ocaml-opt}lib/coq/kernel/primred.cmx
 lib/coq/kernel/reduction.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/reduction.cmx
+lib/coq/kernel/relevanceops.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/relevanceops.cmx
 lib/coq/kernel/retroknowledge.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/retroknowledge.cmx
-lib/coq/kernel/retypeops.cmi
-${PLIST.ocaml-opt}lib/coq/kernel/retypeops.cmx
 lib/coq/kernel/safe_typing.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/safe_typing.cmx
+lib/coq/kernel/section.cmi
+${PLIST.ocaml-opt}lib/coq/kernel/section.cmx
 lib/coq/kernel/sorts.cmi
 ${PLIST.ocaml-opt}lib/coq/kernel/sorts.cmx
 lib/coq/kernel/subtyping.cmi
@@ -360,6 +365,8 @@
 ${PLIST.ocaml-opt}lib/coq/lib/lib.cmxa
 lib/coq/lib/loc.cmi
 ${PLIST.ocaml-opt}lib/coq/lib/loc.cmx
+lib/coq/lib/objFile.cmi
+${PLIST.ocaml-opt}lib/coq/lib/objFile.cmx
 lib/coq/lib/pp.cmi
 ${PLIST.ocaml-opt}lib/coq/lib/pp.cmx
 lib/coq/lib/pp_diff.cmi
@@ -379,22 +386,12 @@
 lib/coq/lib/xml_datatype.cmi
 lib/coq/library/coqlib.cmi
 ${PLIST.ocaml-opt}lib/coq/library/coqlib.cmx
-lib/coq/library/decl_kinds.cmi
-${PLIST.ocaml-opt}lib/coq/library/decl_kinds.cmx
-lib/coq/library/declaremods.cmi
-${PLIST.ocaml-opt}lib/coq/library/declaremods.cmx
-lib/coq/library/decls.cmi
-${PLIST.ocaml-opt}lib/coq/library/decls.cmx
 lib/coq/library/global.cmi
 ${PLIST.ocaml-opt}lib/coq/library/global.cmx
 lib/coq/library/globnames.cmi
 ${PLIST.ocaml-opt}lib/coq/library/globnames.cmx
 lib/coq/library/goptions.cmi
 ${PLIST.ocaml-opt}lib/coq/library/goptions.cmx
-lib/coq/library/keys.cmi
-${PLIST.ocaml-opt}lib/coq/library/keys.cmx
-lib/coq/library/kindops.cmi
-${PLIST.ocaml-opt}lib/coq/library/kindops.cmx
 lib/coq/library/lib.cmi
 ${PLIST.ocaml-opt}lib/coq/library/lib.cmx
 lib/coq/library/libnames.cmi
@@ -402,11 +399,7 @@
 lib/coq/library/libobject.cmi
 ${PLIST.ocaml-opt}lib/coq/library/libobject.cmx
 ${PLIST.ocaml-opt}lib/coq/library/library.a
-lib/coq/library/library.cmi
-${PLIST.ocaml-opt}lib/coq/library/library.cmx
 ${PLIST.ocaml-opt}lib/coq/library/library.cmxa
-lib/coq/library/loadpath.cmi
-${PLIST.ocaml-opt}lib/coq/library/loadpath.cmx
 lib/coq/library/nametab.cmi
 ${PLIST.ocaml-opt}lib/coq/library/nametab.cmx
 lib/coq/library/states.cmi
@@ -433,27 +426,6 @@
 ${PLIST.ocaml-opt}lib/coq/parsing/ppextend.cmx
 lib/coq/parsing/tok.cmi
 ${PLIST.ocaml-opt}lib/coq/parsing/tok.cmx
-lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
-${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.o
-lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmx
-${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.o
-lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmx
-${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.o
-lib/coq/plugins/btauto/Algebra.glob
-lib/coq/plugins/btauto/Algebra.v
-lib/coq/plugins/btauto/Algebra.vo
-lib/coq/plugins/btauto/Btauto.glob
-lib/coq/plugins/btauto/Btauto.v
-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.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/btauto/btauto_plugin.cmx
 ${PLIST.natdynlink}lib/coq/plugins/btauto/btauto_plugin.cmxs
@@ -472,13 +444,6 @@
 lib/coq/plugins/cc/cctac.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/cc/cctac.cmx
 ${PLIST.ocaml-opt}lib/coq/plugins/cc/g_congruence.cmx
-lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmx
-${PLIST.natdynlink}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.o
-lib/coq/plugins/derive/Derive.glob
-lib/coq/plugins/derive/Derive.v
-lib/coq/plugins/derive/Derive.vo
 lib/coq/plugins/derive/derive.cmi
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/derive.cmx
 lib/coq/plugins/derive/derive_plugin.cmi
@@ -486,132 +451,6 @@
 ${PLIST.natdynlink}lib/coq/plugins/derive/derive_plugin.cmxs
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/derive_plugin.o
 ${PLIST.ocaml-opt}lib/coq/plugins/derive/g_derive.cmx
-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
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOCamlInt63.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.o
-lib/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmx
-${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.o
-lib/coq/plugins/extraction/ExtrHaskellBasic.glob
-lib/coq/plugins/extraction/ExtrHaskellBasic.v
-lib/coq/plugins/extraction/ExtrHaskellBasic.vo
-lib/coq/plugins/extraction/ExtrHaskellNatInt.glob
-lib/coq/plugins/extraction/ExtrHaskellNatInt.v
-lib/coq/plugins/extraction/ExtrHaskellNatInt.vo
-lib/coq/plugins/extraction/ExtrHaskellNatInteger.glob
-lib/coq/plugins/extraction/ExtrHaskellNatInteger.v
-lib/coq/plugins/extraction/ExtrHaskellNatInteger.vo
-lib/coq/plugins/extraction/ExtrHaskellNatNum.glob
-lib/coq/plugins/extraction/ExtrHaskellNatNum.v
-lib/coq/plugins/extraction/ExtrHaskellNatNum.vo
-lib/coq/plugins/extraction/ExtrHaskellString.glob
Prev by Date: [pkgsrc/trunk]: pkgsrc/doc CHANGES for tex-tabulary and coq
Next by Date: [pkgsrc/trunk]: pkgsrc/print +tex-tabulary
Previous by Thread: [pkgsrc/trunk]: pkgsrc/doc CHANGES for tex-tabulary and coq
Next by Thread: [pkgsrc/trunk]: pkgsrc/print +tex-tabulary
Indexes:
Home | Main Index | Thread Index | Old Index