pkgsrc-Changes-HG archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]

[pkgsrc/trunk]: pkgsrc/lang/coq Updated package to latest version, 8.6.1. Cha...

details:   https://anonhg.NetBSD.org/pkgsrc/rev/057a3439a79c
branches:  trunk
changeset: 367943:057a3439a79c
user:      jaapb <jaapb%pkgsrc.org@localhost>
date:      Fri Sep 08 17:19:01 2017 +0000

description:
Updated package to latest version, 8.6.1. Changes include:

- Fix #5380: Default colors for CoqIDE are actually applied.
- Fix plugin warnings
- Document named evars (including Show ident)
- Fix Bug #5574, document function scope
- Adding a test case as requested in bug 5205.
- Fix Bug #5568, no dup notation warnings on repeated module imports
- Fix documentation of Typeclasses eauto :=
- Refactor documentation of records.
- Protecting from warnings while compiling 8.6
- Fixing an inconsistency between configure and configure.ml
- Add test-suite checks for coqchk with constraints
- Fix bug #5019 (looping zify on dependent types)
- Fix bug 5550: "typeclasses eauto with" does not work with section variables.
- Bug 5546, qualify datatype constructors when needed in Show Match
- Bug #5535, test for Show with -emacs
- Fix bug #5486, don't reverse ids in tuples
- Fixing #5522 (anomaly with free vars of pat)
- Fix bug #5526, don't check for nonlinearity in notation if printing only
- Fix bug #5255
- Fix bug #3659: -time should understand multibyte encodings.
- FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print Assumptions".
- Fix outdated description in RefMan.
- Repairing `Set Rewriting Schemes`
- Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
- Fix description of command-line arguments for Add (Rec) LoadPath
- Fix bug #5377: @? patterns broken.
- add XML protocol doc
- Fix anomaly when doing [all:Check _.] during a proof.
- Correction of bug #4306
- Fix #5435: [Eval native_compute in] raises anomaly.
- Instances should obey universe binders even when defined by tactics.
- Intern names bound in match patterns
- funind: Ignore missing info for current function
- Do not typecheck twice the type of opaque constants.
- show unused intro pattern warning
- [future] Be eager when "chaining" already resolved future values.
- Opaque side effects
- Fix #5132: coq_makefile generates incorrect install goal
- Run non-tactic comands without resilient_command
- Univs: fix bug #5365, generation of u+k <= v constraints
- make `emit' tail recursive
- Don't require printing-only notation to be productive
- Fix the way setoid_rewrite handles bindings.
- Fix for bug 5244 - set printing width ignored when given enough space
- Fix bug 4969, autoapply was not tagging shelved subgoals correctly

diffstat:

 lang/coq/Makefile |    10 +-
 lang/coq/PLIST    |  3971 ++++++++++++++++++++++++++--------------------------
 lang/coq/distinfo |    10 +-
 3 files changed, 2010 insertions(+), 1981 deletions(-)

diffs (truncated from 4375 to 300 lines):

diff -r 92a5cd7c627a -r 057a3439a79c lang/coq/Makefile
--- a/lang/coq/Makefile Fri Sep 08 17:14:34 2017 +0000
+++ b/lang/coq/Makefile Fri Sep 08 17:19:01 2017 +0000
@@ -1,8 +1,7 @@
-# $NetBSD: Makefile,v 1.98 2017/07/11 14:19:20 jaapb Exp $
+# $NetBSD: Makefile,v 1.99 2017/09/08 17:19:01 jaapb Exp $
 #
 
-DISTNAME=      coq-8.6
-PKGREVISION=   4
+DISTNAME=      coq-8.6.1
 CATEGORIES=    lang math
 MASTER_SITES=  http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
 
@@ -26,10 +25,15 @@
 .include "../../mk/bsd.prefs.mk"
 .include "../../mk/ocaml.mk"
 
+PLIST_VARS+=   native
 .if ${OCAML_USE_OPT_COMPILER} == "yes"
 PLIST_SUBST+=  COQIDE_TYPE="opt"
+PLIST.native=  yes
+CONFIGURE_ARGS+=       -native-compiler yes
+UNLIMIT_RESOURCES+=    stacksize # compilation of some files needs this
 .else
 PLIST_SUBST+=  COQIDE_TYPE="byte"
+CONFIGURE_ARGS+=       -native-compiler no
 .endif
 
 .if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
diff -r 92a5cd7c627a -r 057a3439a79c lang/coq/PLIST
--- a/lang/coq/PLIST    Fri Sep 08 17:14:34 2017 +0000
+++ b/lang/coq/PLIST    Fri Sep 08 17:19:01 2017 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.20 2016/12/30 13:23:06 jaapb Exp $
+@comment $NetBSD: PLIST,v 1.21 2017/09/08 17:19:01 jaapb Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -291,18 +291,18 @@
 lib/coq/parsing/parsing.cmxa
 lib/coq/parsing/pcoq.cmi
 lib/coq/parsing/tok.cmi
-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
+${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.o
+${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.o
+${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmxs
+${PLIST.native}${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
@@ -340,70 +340,74 @@
 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/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_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
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInteger.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatNum.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellString.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInt.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZInteger.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellZNum.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBasic.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlBigIntConv.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlIntConv.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatBigInt.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlNatInt.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlString.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZBigInt.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrOcamlZInt.o
+${PLIST.native}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/extraction/.coq-native/NCoq_extraction_Extraction.cmxs
+${PLIST.native}${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
@@ -452,6 +456,9 @@
 lib/coq/plugins/extraction/ExtrOcamlZInt.glob
 lib/coq/plugins/extraction/ExtrOcamlZInt.v
 lib/coq/plugins/extraction/ExtrOcamlZInt.vo
+lib/coq/plugins/extraction/Extraction.glob
+lib/coq/plugins/extraction/Extraction.v
+lib/coq/plugins/extraction/Extraction.vo
 lib/coq/plugins/extraction/common.cmi
 lib/coq/plugins/extraction/extract_env.cmi
 lib/coq/plugins/extraction/extraction.cmi
@@ -475,14 +482,14 @@
 lib/coq/plugins/firstorder/rules.cmi
 lib/coq/plugins/firstorder/sequent.cmi
 lib/coq/plugins/firstorder/unify.cmi
-lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmx
-${PLIST.natdynlink}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.o
-lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmx
-${PLIST.natdynlink}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.o
+${PLIST.native}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier.o
+${PLIST.native}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/fourier/.coq-native/NCoq_fourier_Fourier_util.o
 lib/coq/plugins/fourier/Fourier.glob
 lib/coq/plugins/fourier/Fourier.v
 lib/coq/plugins/fourier/Fourier.vo
@@ -492,10 +499,17 @@
 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/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
-${PLIST.ocaml-opt}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.o
+${PLIST.native}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.o
+${PLIST.native}lib/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmi
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmx
+${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.cmxs
+${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/funind/.coq-native/NCoq_funind_FunInd.o
+lib/coq/plugins/funind/FunInd.glob
+lib/coq/plugins/funind/FunInd.v
+lib/coq/plugins/funind/FunInd.vo
 lib/coq/plugins/funind/Recdef.glob
 lib/coq/plugins/funind/Recdef.v
 lib/coq/plugins/funind/Recdef.vo
@@ -509,66 +523,77 @@
 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/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
-${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.o
-lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmx
-${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.o
-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
-${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.o
-lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmx
-${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.o
-lib/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.cmi
-${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.cmx
-${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.cmxs
-${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_QMicromega.o
Home | Main Index | Thread Index | Old Index