Updated lang/coq to version 8.7.0.
Includes many improvements and bugfixes (none that seem to be breaking backwards compatibility though), see the CHANGELOG. For packaging: - camlp4 support removed, package now uses camlp5 exclusively - fix for PR pkg/52651
This commit is contained in:
jaapb
parent
dae1357d93
commit
e033a835ab
5 changed files with 233 additions and 357 deletions
|
|
@ -1,8 +1,7 @@
|
|||
# $NetBSD: Makefile,v 1.100 2017/09/18 09:53:24 maya Exp $
|
||||
# $NetBSD: Makefile,v 1.101 2017/11/03 11:20:28 jaapb Exp $
|
||||
#
|
||||
|
||||
DISTNAME= coq-8.6.1
|
||||
PKGREVISION= 1
|
||||
DISTNAME= coq-8.7.0
|
||||
CATEGORIES= lang math
|
||||
MASTER_SITES= http://coq.inria.fr/distrib/V${PKGVERSION_NOREV}/files/
|
||||
|
||||
|
|
@ -19,7 +18,6 @@ CONFIGURE_ARGS+= -mandir ${PREFIX}/${PKGMANDIR}
|
|||
CONFIGURE_ARGS+= -configdir ${PKG_SYSCONFDIR}/xdg/coq
|
||||
CONFIGURE_ARGS+= -docdir ${PREFIX}/share/doc/coq
|
||||
CONFIGURE_ARGS+= -coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq
|
||||
BUILD_TARGET= world
|
||||
|
||||
BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10
|
||||
|
||||
|
|
@ -32,9 +30,12 @@ PLIST_SUBST+= COQIDE_TYPE="opt"
|
|||
PLIST.native= yes
|
||||
CONFIGURE_ARGS+= -native-compiler yes
|
||||
UNLIMIT_RESOURCES+= stacksize # compilation of some files needs this
|
||||
BUILD_TARGET= world
|
||||
.else
|
||||
PLIST_SUBST+= COQIDE_TYPE="byte"
|
||||
CONFIGURE_ARGS+= -native-compiler no
|
||||
BUILD_TARGET= byte
|
||||
INSTALL_TARGET= install-byte
|
||||
.endif
|
||||
|
||||
.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
|
||||
|
|
@ -47,7 +48,17 @@ PLIST.natdynlink= yes
|
|||
. endif
|
||||
.endif
|
||||
|
||||
.include "../../lang/python/pyversion.mk"
|
||||
|
||||
REPLACE_SH= configure install.sh
|
||||
REPLACE_INTERPRETER+= python
|
||||
REPLACE.python.old= python
|
||||
REPLACE.python.new= ${PYTHONBIN}
|
||||
REPLACE_FILES.python= tools/TimeFileMaker.py \
|
||||
tools/make-both-single-timing-files.py \
|
||||
tools/make-both-time-files.py \
|
||||
tools/make-one-time-file.py
|
||||
|
||||
INSTALL_ENV+= COQINSTALLPREFIX=${DESTDIR}
|
||||
|
||||
PLIST_VARS+= coqide natdynlink doc
|
||||
|
|
@ -63,6 +74,7 @@ SUBST_MESSAGE.fix-paths= Remove buildlink references from Coq_config module
|
|||
SUBST_FILES.fix-paths= config/coq_config.ml
|
||||
SUBST_SED.fix-paths= -e "s,${BUILDLINK_DIR},${PREFIX},g"
|
||||
|
||||
.include "../../lang/camlp4/buildlink3.mk"
|
||||
|
||||
.include "../../lang/camlp5/buildlink3.mk"
|
||||
.include "../../mk/pthread.buildlink3.mk"
|
||||
.include "../../mk/bsd.pkg.mk"
|
||||
|
|
|
|||
529
lang/coq/PLIST
529
lang/coq/PLIST
|
|
@ -1,4 +1,4 @@
|
|||
@comment $NetBSD: PLIST,v 1.21 2017/09/08 17:19:01 jaapb Exp $
|
||||
@comment $NetBSD: PLIST,v 1.22 2017/11/03 11:20:28 jaapb Exp $
|
||||
bin/coq-tex
|
||||
bin/coq_makefile
|
||||
bin/coqc
|
||||
|
|
@ -8,14 +8,13 @@ bin/coqdoc
|
|||
${PLIST.coqide}bin/coqide
|
||||
bin/coqmktop
|
||||
bin/coqtop
|
||||
bin/coqtop.byte
|
||||
bin/coqwc
|
||||
bin/coqworkmgr
|
||||
bin/gallina
|
||||
lib/coq/META
|
||||
lib/coq/dllcoqrun.so
|
||||
lib/coq/config/coq_config.cmi
|
||||
lib/coq/engine/eConstr.cmi
|
||||
${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
|
||||
|
|
@ -25,13 +24,12 @@ 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/engine/universes.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
|
||||
|
|
@ -42,28 +40,21 @@ ${PLIST.coqide}lib/coq/ide/coqide_ui.cmi
|
|||
${PLIST.coqide}lib/coq/ide/document.cmi
|
||||
${PLIST.coqide}lib/coq/ide/fileOps.cmi
|
||||
${PLIST.coqide}lib/coq/ide/gtk_parsing.cmi
|
||||
${PLIST.coqide}lib/coq/ide/ide.a
|
||||
${PLIST.coqide}lib/coq/ide/ide.cma
|
||||
${PLIST.coqide}lib/coq/ide/ide.cmxa
|
||||
${PLIST.coqide}${PLIST.ocaml-opt}lib/coq/ide/ide.a
|
||||
${PLIST.coqide}${PLIST.ocaml-opt}lib/coq/ide/ide.cmxa
|
||||
${PLIST.coqide}lib/coq/ide/ideutils.cmi
|
||||
${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/richpp.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/session.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
|
||||
${PLIST.coqide}lib/coq/ide/utils/configwin.cmi
|
||||
${PLIST.coqide}lib/coq/ide/utils/configwin_ihm.cmi
|
||||
${PLIST.coqide}lib/coq/ide/utils/configwin_keys.cmi
|
||||
${PLIST.coqide}lib/coq/ide/utils/configwin_messages.cmi
|
||||
${PLIST.coqide}lib/coq/ide/utils/configwin_types.cmi
|
||||
${PLIST.coqide}lib/coq/ide/utils/editable_cells.cmi
|
||||
${PLIST.coqide}lib/coq/ide/utils/okey.cmi
|
||||
${PLIST.coqide}lib/coq/ide/wg_Command.cmi
|
||||
${PLIST.coqide}lib/coq/ide/wg_Completion.cmi
|
||||
${PLIST.coqide}lib/coq/ide/wg_Detachable.cmi
|
||||
|
|
@ -73,21 +64,20 @@ ${PLIST.coqide}lib/coq/ide/wg_Notebook.cmi
|
|||
${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
|
||||
${PLIST.coqide}lib/coq/ide/xmlprotocol.cmi
|
||||
lib/coq/interp/constrexpr_ops.cmi
|
||||
lib/coq/interp/constrextern.cmi
|
||||
lib/coq/interp/constrintern.cmi
|
||||
lib/coq/interp/coqlib.cmi
|
||||
lib/coq/interp/declare.cmi
|
||||
lib/coq/interp/dumpglob.cmi
|
||||
lib/coq/interp/genintern.cmi
|
||||
lib/coq/interp/impargs.cmi
|
||||
lib/coq/interp/implicit_quantifiers.cmi
|
||||
lib/coq/interp/interp.a
|
||||
lib/coq/interp/interp.cma
|
||||
lib/coq/interp/interp.cmxa
|
||||
${PLIST.ocaml-opt}lib/coq/interp/interp.a
|
||||
${PLIST.ocaml-opt}lib/coq/interp/interp.cmxa
|
||||
lib/coq/interp/modintern.cmi
|
||||
lib/coq/interp/notation.cmi
|
||||
lib/coq/interp/notation_ops.cmi
|
||||
|
|
@ -103,12 +93,16 @@ lib/coq/intf/evar_kinds.cmi
|
|||
lib/coq/intf/extend.cmi
|
||||
lib/coq/intf/genredexpr.cmi
|
||||
lib/coq/intf/glob_term.cmi
|
||||
${PLIST.ocaml-opt}lib/coq/intf/intf.a
|
||||
${PLIST.ocaml-opt}lib/coq/intf/intf.cmxa
|
||||
lib/coq/intf/locus.cmi
|
||||
lib/coq/intf/misctypes.cmi
|
||||
lib/coq/intf/notation_term.cmi
|
||||
lib/coq/intf/pattern.cmi
|
||||
lib/coq/intf/tacexpr.cmi
|
||||
lib/coq/intf/tactypes.cmi
|
||||
lib/coq/intf/vernacexpr.cmi
|
||||
lib/coq/kernel/byterun/dllcoqrun.so
|
||||
lib/coq/kernel/byterun/libcoqrun.a
|
||||
lib/coq/kernel/cClosure.cmi
|
||||
lib/coq/kernel/cbytecodes.cmi
|
||||
lib/coq/kernel/cbytegen.cmi
|
||||
|
|
@ -125,12 +119,10 @@ lib/coq/kernel/entries.cmi
|
|||
lib/coq/kernel/environ.cmi
|
||||
lib/coq/kernel/esubst.cmi
|
||||
lib/coq/kernel/evar.cmi
|
||||
lib/coq/kernel/fast_typeops.cmi
|
||||
lib/coq/kernel/indtypes.cmi
|
||||
lib/coq/kernel/inductive.cmi
|
||||
lib/coq/kernel/kernel.a
|
||||
lib/coq/kernel/kernel.cma
|
||||
lib/coq/kernel/kernel.cmxa
|
||||
${PLIST.ocaml-opt}lib/coq/kernel/kernel.a
|
||||
${PLIST.ocaml-opt}lib/coq/kernel/kernel.cmxa
|
||||
lib/coq/kernel/mod_subst.cmi
|
||||
lib/coq/kernel/mod_typing.cmi
|
||||
lib/coq/kernel/modops.cmi
|
||||
|
|
@ -164,6 +156,7 @@ lib/coq/lib/aux_file.cmi
|
|||
lib/coq/lib/backtrace.cmi
|
||||
lib/coq/lib/bigint.cmi
|
||||
lib/coq/lib/cArray.cmi
|
||||
lib/coq/lib/cAst.cmi
|
||||
lib/coq/lib/cEphemeron.cmi
|
||||
lib/coq/lib/cErrors.cmi
|
||||
lib/coq/lib/cList.cmi
|
||||
|
|
@ -177,10 +170,10 @@ 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
|
||||
lib/coq/lib/clib.cmxa
|
||||
${PLIST.ocaml-opt}lib/coq/lib/clib.a
|
||||
${PLIST.ocaml-opt}lib/coq/lib/clib.cmxa
|
||||
lib/coq/lib/control.cmi
|
||||
lib/coq/lib/coqProject_file.cmi
|
||||
lib/coq/lib/deque.cmi
|
||||
lib/coq/lib/dyn.cmi
|
||||
lib/coq/lib/envars.cmi
|
||||
|
|
@ -197,20 +190,16 @@ lib/coq/lib/heap.cmi
|
|||
lib/coq/lib/hook.cmi
|
||||
lib/coq/lib/iStream.cmi
|
||||
lib/coq/lib/int.cmi
|
||||
lib/coq/lib/lib.a
|
||||
lib/coq/lib/lib.cma
|
||||
lib/coq/lib/lib.cmxa
|
||||
${PLIST.ocaml-opt}lib/coq/lib/lib.a
|
||||
${PLIST.ocaml-opt}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
|
||||
lib/coq/lib/pp_control.cmi
|
||||
lib/coq/lib/ppstyle.cmi
|
||||
lib/coq/lib/predicate.cmi
|
||||
lib/coq/lib/profile.cmi
|
||||
lib/coq/lib/remoteCounter.cmi
|
||||
lib/coq/lib/richpp.cmi
|
||||
lib/coq/lib/rtree.cmi
|
||||
lib/coq/lib/segmenttree.cmi
|
||||
lib/coq/lib/spawn.cmi
|
||||
|
|
@ -224,8 +213,7 @@ lib/coq/lib/unicodetable.cmi
|
|||
lib/coq/lib/unionfind.cmi
|
||||
lib/coq/lib/util.cmi
|
||||
lib/coq/lib/xml_datatype.cmi
|
||||
lib/coq/libcoqrun.a
|
||||
lib/coq/library/declare.cmi
|
||||
lib/coq/library/coqlib.cmi
|
||||
lib/coq/library/declaremods.cmi
|
||||
lib/coq/library/decls.cmi
|
||||
lib/coq/library/dischargedhypsmap.cmi
|
||||
|
|
@ -233,62 +221,31 @@ lib/coq/library/global.cmi
|
|||
lib/coq/library/globnames.cmi
|
||||
lib/coq/library/goptions.cmi
|
||||
lib/coq/library/heads.cmi
|
||||
lib/coq/library/impargs.cmi
|
||||
lib/coq/library/keys.cmi
|
||||
lib/coq/library/kindops.cmi
|
||||
lib/coq/library/lib.cmi
|
||||
lib/coq/library/libnames.cmi
|
||||
lib/coq/library/libobject.cmi
|
||||
lib/coq/library/library.a
|
||||
lib/coq/library/library.cma
|
||||
${PLIST.ocaml-opt}lib/coq/library/library.a
|
||||
lib/coq/library/library.cmi
|
||||
lib/coq/library/library.cmxa
|
||||
${PLIST.ocaml-opt}lib/coq/library/library.cmxa
|
||||
lib/coq/library/loadpath.cmi
|
||||
lib/coq/library/nameops.cmi
|
||||
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/library/univops.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_prim.cmi
|
||||
lib/coq/parsing/g_proofs.cmi
|
||||
lib/coq/parsing/g_tactic.cmi
|
||||
lib/coq/parsing/g_vernac.cmi
|
||||
lib/coq/parsing/highparsing.a
|
||||
lib/coq/parsing/highparsing.cma
|
||||
lib/coq/parsing/highparsing.cmxa
|
||||
lib/coq/parsing/parsing.a
|
||||
lib/coq/parsing/parsing.cma
|
||||
lib/coq/parsing/parsing.cmxa
|
||||
${PLIST.ocaml-opt}lib/coq/parsing/highparsing.a
|
||||
${PLIST.ocaml-opt}lib/coq/parsing/highparsing.cmxa
|
||||
${PLIST.ocaml-opt}lib/coq/parsing/parsing.a
|
||||
${PLIST.ocaml-opt}lib/coq/parsing/parsing.cmxa
|
||||
lib/coq/parsing/pcoq.cmi
|
||||
lib/coq/parsing/tok.cmi
|
||||
${PLIST.native}lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
|
||||
|
|
@ -313,32 +270,21 @@ 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
|
||||
lib/coq/plugins/btauto/btauto_plugin.cmo
|
||||
lib/coq/plugins/btauto/btauto_plugin.cmxs
|
||||
${PLIST.natdynlink}lib/coq/plugins/btauto/btauto_plugin.cmxs
|
||||
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/ccalgo.cmi
|
||||
lib/coq/plugins/cc/ccproof.cmi
|
||||
lib/coq/plugins/cc/cctac.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.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_proof_instr.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
|
||||
lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmxs
|
||||
${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
|
||||
lib/coq/plugins/derive/derive_plugin.cmi
|
||||
lib/coq/plugins/derive/derive_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/derive/derive_plugin.cmxs
|
||||
${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
|
||||
|
|
@ -463,7 +409,6 @@ 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.cmi
|
||||
lib/coq/plugins/extraction/extraction_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/extraction/extraction_plugin.cmxs
|
||||
lib/coq/plugins/extraction/haskell.cmi
|
||||
lib/coq/plugins/extraction/json.cmi
|
||||
|
|
@ -476,7 +421,6 @@ lib/coq/plugins/extraction/table.cmi
|
|||
lib/coq/plugins/firstorder/formula.cmi
|
||||
lib/coq/plugins/firstorder/ground.cmi
|
||||
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/instances.cmi
|
||||
lib/coq/plugins/firstorder/rules.cmi
|
||||
|
|
@ -497,7 +441,6 @@ 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_plugin.cmi
|
||||
lib/coq/plugins/fourier/fourier_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/fourier/fourier_plugin.cmxs
|
||||
${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
|
||||
|
|
@ -521,23 +464,41 @@ lib/coq/plugins/funind/indfun.cmi
|
|||
lib/coq/plugins/funind/indfun_common.cmi
|
||||
lib/coq/plugins/funind/recdef.cmi
|
||||
lib/coq/plugins/funind/recdef_plugin.cmi
|
||||
lib/coq/plugins/funind/recdef_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/funind/recdef_plugin.cmxs
|
||||
${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.o
|
||||
${PLIST.native}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_LtacDummy.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_LtacDummy.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_LtacDummy.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_LtacDummy.o
|
||||
lib/coq/plugins/ltac/LtacDummy.glob
|
||||
lib/coq/plugins/ltac/LtacDummy.v
|
||||
lib/coq/plugins/ltac/LtacDummy.vo
|
||||
lib/coq/plugins/ltac/ltac_dummy.cmi
|
||||
lib/coq/plugins/ltac/ltac_plugin.cmi
|
||||
lib/coq/plugins/ltac/ltac_plugin.cmo
|
||||
lib/coq/plugins/ltac/ltac_plugin.cmxs
|
||||
${PLIST.natdynlink}lib/coq/plugins/ltac/ltac_plugin.cmxs
|
||||
${PLIST.native}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ltac/.coq-native/NCoq_ltac_Ltac.o
|
||||
lib/coq/plugins/ltac/Ltac.glob
|
||||
lib/coq/plugins/ltac/Ltac.v
|
||||
lib/coq/plugins/ltac/Ltac.vo
|
||||
lib/coq/plugins/ltac/evar_tactics.cmi
|
||||
lib/coq/plugins/ltac/extraargs.cmi
|
||||
lib/coq/plugins/ltac/extratactics.cmi
|
||||
lib/coq/plugins/ltac/pltac.cmi
|
||||
lib/coq/plugins/ltac/pptactic.cmi
|
||||
lib/coq/plugins/ltac/profile_ltac.cmi
|
||||
lib/coq/plugins/ltac/rewrite.cmi
|
||||
lib/coq/plugins/ltac/tacarg.cmi
|
||||
lib/coq/plugins/ltac/taccoerce.cmi
|
||||
lib/coq/plugins/ltac/tacentries.cmi
|
||||
lib/coq/plugins/ltac/tacenv.cmi
|
||||
lib/coq/plugins/ltac/tacexpr.cmi
|
||||
lib/coq/plugins/ltac/tacintern.cmi
|
||||
lib/coq/plugins/ltac/tacinterp.cmi
|
||||
lib/coq/plugins/ltac/tacsubst.cmi
|
||||
lib/coq/plugins/ltac/tactic_debug.cmi
|
||||
lib/coq/plugins/ltac/tactic_matching.cmi
|
||||
lib/coq/plugins/ltac/tactic_option.cmi
|
||||
lib/coq/plugins/ltac/tauto.cmi
|
||||
lib/coq/plugins/ltac/tauto_plugin.cmi
|
||||
${PLIST.natdynlink}lib/coq/plugins/ltac/tauto_plugin.cmxs
|
||||
${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmxs
|
||||
|
|
@ -554,6 +515,10 @@ ${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi
|
|||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.o
|
||||
${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_MExtraction.o
|
||||
${PLIST.native}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmxs
|
||||
|
|
@ -609,6 +574,9 @@ 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/MExtraction.glob
|
||||
lib/coq/plugins/micromega/MExtraction.v
|
||||
lib/coq/plugins/micromega/MExtraction.vo
|
||||
lib/coq/plugins/micromega/OrderedRing.glob
|
||||
lib/coq/plugins/micromega/OrderedRing.v
|
||||
lib/coq/plugins/micromega/OrderedRing.vo
|
||||
|
|
@ -642,9 +610,9 @@ lib/coq/plugins/micromega/ZMicromega.vo
|
|||
lib/coq/plugins/micromega/csdpcert
|
||||
lib/coq/plugins/micromega/micromega.cmi
|
||||
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/sos.cmi
|
||||
lib/coq/plugins/micromega/sos_types.cmi
|
||||
${PLIST.native}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmxs
|
||||
|
|
@ -655,7 +623,6 @@ lib/coq/plugins/nsatz/Nsatz.vo
|
|||
lib/coq/plugins/nsatz/ideal.cmi
|
||||
lib/coq/plugins/nsatz/nsatz.cmi
|
||||
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/polynom.cmi
|
||||
lib/coq/plugins/nsatz/utile.cmi
|
||||
|
|
@ -695,7 +662,6 @@ lib/coq/plugins/omega/PreOmega.glob
|
|||
lib/coq/plugins/omega/PreOmega.v
|
||||
lib/coq/plugins/omega/PreOmega.vo
|
||||
lib/coq/plugins/omega/omega_plugin.cmi
|
||||
lib/coq/plugins/omega/omega_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/omega/omega_plugin.cmxs
|
||||
${PLIST.native}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmx
|
||||
|
|
@ -705,7 +671,6 @@ lib/coq/plugins/quote/Quote.glob
|
|||
lib/coq/plugins/quote/Quote.v
|
||||
lib/coq/plugins/quote/Quote.vo
|
||||
lib/coq/plugins/quote/quote_plugin.cmi
|
||||
lib/coq/plugins/quote/quote_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/quote/quote_plugin.cmxs
|
||||
${PLIST.native}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmx
|
||||
|
|
@ -723,7 +688,6 @@ lib/coq/plugins/romega/ReflOmegaCore.v
|
|||
lib/coq/plugins/romega/ReflOmegaCore.vo
|
||||
lib/coq/plugins/romega/const_omega.cmi
|
||||
lib/coq/plugins/romega/romega_plugin.cmi
|
||||
lib/coq/plugins/romega/romega_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/romega/romega_plugin.cmxs
|
||||
${PLIST.native}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmx
|
||||
|
|
@ -742,7 +706,6 @@ lib/coq/plugins/rtauto/Rtauto.vo
|
|||
lib/coq/plugins/rtauto/proof_search.cmi
|
||||
lib/coq/plugins/rtauto/refl_tauto.cmi
|
||||
lib/coq/plugins/rtauto/rtauto_plugin.cmi
|
||||
lib/coq/plugins/rtauto/rtauto_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/rtauto/rtauto_plugin.cmxs
|
||||
${PLIST.native}lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmx
|
||||
|
|
@ -915,8 +878,42 @@ lib/coq/plugins/setoid_ring/ZArithRing.vo
|
|||
lib/coq/plugins/setoid_ring/newring.cmi
|
||||
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
|
||||
${PLIST.native}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrbool.o
|
||||
${PLIST.native}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssreflect.o
|
||||
${PLIST.native}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssr/.coq-native/NCoq_ssr_ssrfun.o
|
||||
lib/coq/plugins/ssr/ssrast.cmi
|
||||
lib/coq/plugins/ssr/ssrbool.glob
|
||||
lib/coq/plugins/ssr/ssrbool.v
|
||||
lib/coq/plugins/ssr/ssrbool.vo
|
||||
lib/coq/plugins/ssr/ssrbwd.cmi
|
||||
lib/coq/plugins/ssr/ssrcommon.cmi
|
||||
lib/coq/plugins/ssr/ssreflect.glob
|
||||
lib/coq/plugins/ssr/ssreflect.v
|
||||
lib/coq/plugins/ssr/ssreflect.vo
|
||||
lib/coq/plugins/ssr/ssreflect_plugin.cmi
|
||||
lib/coq/plugins/ssr/ssreflect_plugin.cmxs
|
||||
lib/coq/plugins/ssr/ssrelim.cmi
|
||||
lib/coq/plugins/ssr/ssrequality.cmi
|
||||
lib/coq/plugins/ssr/ssrfun.glob
|
||||
lib/coq/plugins/ssr/ssrfun.v
|
||||
lib/coq/plugins/ssr/ssrfun.vo
|
||||
lib/coq/plugins/ssr/ssrfwd.cmi
|
||||
lib/coq/plugins/ssr/ssripats.cmi
|
||||
lib/coq/plugins/ssr/ssrparser.cmi
|
||||
lib/coq/plugins/ssr/ssrprinters.cmi
|
||||
lib/coq/plugins/ssr/ssrtacticals.cmi
|
||||
lib/coq/plugins/ssr/ssrvernac.cmi
|
||||
lib/coq/plugins/ssr/ssrview.cmi
|
||||
${PLIST.native}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmxs
|
||||
|
|
@ -926,25 +923,18 @@ 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/int31_syntax_plugin.cmi
|
||||
${PLIST.natdynlink}lib/coq/plugins/syntax/int31_syntax_plugin.cmxs
|
||||
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/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/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/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/z_syntax_plugin.cmi
|
||||
lib/coq/plugins/syntax/z_syntax_plugin.cmo
|
||||
${PLIST.natdynlink}lib/coq/plugins/syntax/z_syntax_plugin.cmxs
|
||||
lib/coq/pretyping/arguments_renaming.cmi
|
||||
lib/coq/pretyping/cases.cmi
|
||||
|
|
@ -966,7 +956,6 @@ lib/coq/pretyping/nativenorm.cmi
|
|||
lib/coq/pretyping/patternops.cmi
|
||||
lib/coq/pretyping/pretype_errors.cmi
|
||||
${PLIST.ocaml-opt}lib/coq/pretyping/pretyping.a
|
||||
lib/coq/pretyping/pretyping.cma
|
||||
lib/coq/pretyping/pretyping.cmi
|
||||
${PLIST.ocaml-opt}lib/coq/pretyping/pretyping.cmxa
|
||||
lib/coq/pretyping/program.cmi
|
||||
|
|
@ -981,34 +970,26 @@ lib/coq/pretyping/typing.cmi
|
|||
lib/coq/pretyping/unification.cmi
|
||||
lib/coq/pretyping/vnorm.cmi
|
||||
lib/coq/printing/genprint.cmi
|
||||
lib/coq/printing/miscprint.cmi
|
||||
lib/coq/printing/ppannotation.cmi
|
||||
lib/coq/printing/ppconstr.cmi
|
||||
lib/coq/printing/ppconstrsig.cmi
|
||||
lib/coq/printing/pptactic.cmi
|
||||
lib/coq/printing/pptacticsig.cmi
|
||||
lib/coq/printing/pputils.cmi
|
||||
lib/coq/printing/ppvernac.cmi
|
||||
lib/coq/printing/ppvernacsig.cmi
|
||||
lib/coq/printing/prettyp.cmi
|
||||
lib/coq/printing/printer.cmi
|
||||
${PLIST.ocaml-opt}lib/coq/printing/printing.a
|
||||
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/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/miscprint.cmi
|
||||
lib/coq/proofs/pfedit.cmi
|
||||
lib/coq/proofs/proof.cmi
|
||||
lib/coq/proofs/proof_global.cmi
|
||||
lib/coq/proofs/proof_type.cmi
|
||||
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/redexpr.cmi
|
||||
lib/coq/proofs/refine.cmi
|
||||
|
|
@ -1017,10 +998,8 @@ lib/coq/proofs/tacmach.cmi
|
|||
lib/coq/stm/asyncTaskQueue.cmi
|
||||
lib/coq/stm/coqworkmgrApi.cmi
|
||||
lib/coq/stm/dag.cmi
|
||||
lib/coq/stm/lemmas.cmi
|
||||
lib/coq/stm/spawned.cmi
|
||||
${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
|
||||
|
|
@ -1028,6 +1007,7 @@ lib/coq/stm/tQueue.cmi
|
|||
lib/coq/stm/vcs.cmi
|
||||
lib/coq/stm/vernac_classifier.cmi
|
||||
lib/coq/stm/vio_checking.cmi
|
||||
lib/coq/stm/workerLoop.cmi
|
||||
lib/coq/stm/workerPool.cmi
|
||||
lib/coq/tactics/auto.cmi
|
||||
lib/coq/tactics/autorewrite.cmi
|
||||
|
|
@ -1044,12 +1024,11 @@ lib/coq/tactics/eqschemes.cmi
|
|||
lib/coq/tactics/equality.cmi
|
||||
lib/coq/tactics/hints.cmi
|
||||
lib/coq/tactics/hipattern.cmi
|
||||
lib/coq/tactics/ind_tables.cmi
|
||||
lib/coq/tactics/inv.cmi
|
||||
lib/coq/tactics/leminv.cmi
|
||||
lib/coq/tactics/tactic_matching.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/term_dnet.cmi
|
||||
|
|
@ -1366,10 +1345,6 @@ ${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmi
|
|||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_AdmitAxiom.o
|
||||
${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.o
|
||||
${PLIST.native}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmxs
|
||||
|
|
@ -1382,13 +1357,6 @@ lib/coq/theories/Compat/AdmitAxiom.v
|
|||
lib/coq/theories/Compat/AdmitAxiom.glob
|
||||
lib/coq/theories/Compat/AdmitAxiom.v
|
||||
lib/coq/theories/Compat/AdmitAxiom.vo
|
||||
lib/coq/theories/Compat/Coq84.glob
|
||||
lib/coq/theories/Compat/Coq84.v
|
||||
lib/coq/theories/Compat/Coq84.glob
|
||||
lib/coq/theories/Compat/Coq84.v
|
||||
lib/coq/theories/Compat/Coq84.vo
|
||||
lib/coq/theories/Compat/Coq85.glob
|
||||
lib/coq/theories/Compat/Coq85.v
|
||||
lib/coq/theories/Compat/Coq85.glob
|
||||
lib/coq/theories/Compat/Coq85.v
|
||||
lib/coq/theories/Compat/Coq85.vo
|
||||
|
|
@ -1747,6 +1715,10 @@ ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.cmi
|
|||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_Eqdep_dec.o
|
||||
${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalFunctionRepresentative.o
|
||||
${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ExtensionalityFacts.cmxs
|
||||
|
|
@ -1779,6 +1751,18 @@ ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFac
|
|||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFacts.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFacts.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_ProofIrrelevanceFacts.o
|
||||
${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionality.o
|
||||
${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropExtensionalityFacts.o
|
||||
${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_PropFacts.o
|
||||
${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_RelationalChoice.cmxs
|
||||
|
|
@ -1787,6 +1771,10 @@ ${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmi
|
|||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetIsType.o
|
||||
${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_SetoidChoice.o
|
||||
${PLIST.native}lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Logic/.coq-native/NCoq_Logic_WKL.cmxs
|
||||
|
|
@ -1849,6 +1837,9 @@ lib/coq/theories/Logic/EqdepFacts.vo
|
|||
lib/coq/theories/Logic/Eqdep_dec.glob
|
||||
lib/coq/theories/Logic/Eqdep_dec.v
|
||||
lib/coq/theories/Logic/Eqdep_dec.vo
|
||||
lib/coq/theories/Logic/ExtensionalFunctionRepresentative.glob
|
||||
lib/coq/theories/Logic/ExtensionalFunctionRepresentative.v
|
||||
lib/coq/theories/Logic/ExtensionalFunctionRepresentative.vo
|
||||
lib/coq/theories/Logic/ExtensionalityFacts.glob
|
||||
lib/coq/theories/Logic/ExtensionalityFacts.v
|
||||
lib/coq/theories/Logic/ExtensionalityFacts.vo
|
||||
|
|
@ -1873,12 +1864,24 @@ lib/coq/theories/Logic/ProofIrrelevance.vo
|
|||
lib/coq/theories/Logic/ProofIrrelevanceFacts.glob
|
||||
lib/coq/theories/Logic/ProofIrrelevanceFacts.v
|
||||
lib/coq/theories/Logic/ProofIrrelevanceFacts.vo
|
||||
lib/coq/theories/Logic/PropExtensionality.glob
|
||||
lib/coq/theories/Logic/PropExtensionality.v
|
||||
lib/coq/theories/Logic/PropExtensionality.vo
|
||||
lib/coq/theories/Logic/PropExtensionalityFacts.glob
|
||||
lib/coq/theories/Logic/PropExtensionalityFacts.v
|
||||
lib/coq/theories/Logic/PropExtensionalityFacts.vo
|
||||
lib/coq/theories/Logic/PropFacts.glob
|
||||
lib/coq/theories/Logic/PropFacts.v
|
||||
lib/coq/theories/Logic/PropFacts.vo
|
||||
lib/coq/theories/Logic/RelationalChoice.glob
|
||||
lib/coq/theories/Logic/RelationalChoice.v
|
||||
lib/coq/theories/Logic/RelationalChoice.vo
|
||||
lib/coq/theories/Logic/SetIsType.glob
|
||||
lib/coq/theories/Logic/SetIsType.v
|
||||
lib/coq/theories/Logic/SetIsType.vo
|
||||
lib/coq/theories/Logic/SetoidChoice.glob
|
||||
lib/coq/theories/Logic/SetoidChoice.v
|
||||
lib/coq/theories/Logic/SetoidChoice.vo
|
||||
lib/coq/theories/Logic/WKL.glob
|
||||
lib/coq/theories/Logic/WKL.v
|
||||
lib/coq/theories/Logic/WKL.vo
|
||||
|
|
@ -2046,10 +2049,6 @@ lib/coq/theories/NArith/Nnat.vo
|
|||
lib/coq/theories/NArith/Nsqrt_def.glob
|
||||
lib/coq/theories/NArith/Nsqrt_def.v
|
||||
lib/coq/theories/NArith/Nsqrt_def.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BigNumPrelude.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BigNumPrelude.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BigNumPrelude.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BigNumPrelude.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_BinNums.cmxs
|
||||
|
|
@ -2062,9 +2061,6 @@ ${PLIST.native}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmi
|
|||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/.coq-native/NCoq_Numbers_NumPrelude.o
|
||||
lib/coq/theories/Numbers/BigNumPrelude.glob
|
||||
lib/coq/theories/Numbers/BigNumPrelude.v
|
||||
lib/coq/theories/Numbers/BigNumPrelude.vo
|
||||
lib/coq/theories/Numbers/BinNums.glob
|
||||
lib/coq/theories/Numbers/BinNums.v
|
||||
lib/coq/theories/Numbers/BinNums.vo
|
||||
|
|
@ -2072,6 +2068,10 @@ ${PLIST.native}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers
|
|||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_DoubleType.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_NZCyclic.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_NZCyclic.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native/NCoq_Numbers_Cyclic_Abstract_NZCyclic.cmxs
|
||||
|
|
@ -2079,79 +2079,12 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Abstract/.coq-n
|
|||
lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.glob
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/DoubleType.glob
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/DoubleType.v
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/DoubleType.vo
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.glob
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.v
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleAdd.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleAdd.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleAdd.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleAdd.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleBase.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleBase.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleBase.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleBase.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleCyclic.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleCyclic.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleCyclic.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleCyclic.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDiv.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDiv.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDiv.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDiv.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDivn1.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDivn1.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDivn1.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleDivn1.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleLift.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleLift.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleLift.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleLift.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleMul.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleMul.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleMul.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleMul.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSqrt.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSqrt.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSqrt.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSqrt.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSub.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSub.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSub.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleSub.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleType.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleType.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleType.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/DoubleCyclic/.coq-native/NCoq_Numbers_Cyclic_DoubleCyclic_DoubleType.o
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.glob
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Cyclic/Int31/.coq-native/NCoq_Numbers_Cyclic_Int31_Cyclic31.cmxs
|
||||
|
|
@ -2306,20 +2239,6 @@ lib/coq/theories/Numbers/Integer/Abstract/ZProperties.vo
|
|||
lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.glob
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.v
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_BigZ.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_BigZ.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_BigZ.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_BigZ.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_ZMake.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_ZMake.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_ZMake.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/BigZ/.coq-native/NCoq_Numbers_Integer_BigZ_ZMake.o
|
||||
lib/coq/theories/Numbers/Integer/BigZ/BigZ.glob
|
||||
lib/coq/theories/Numbers/Integer/BigZ/BigZ.v
|
||||
lib/coq/theories/Numbers/Integer/BigZ/BigZ.vo
|
||||
lib/coq/theories/Numbers/Integer/BigZ/ZMake.glob
|
||||
lib/coq/theories/Numbers/Integer/BigZ/ZMake.v
|
||||
lib/coq/theories/Numbers/Integer/BigZ/ZMake.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Integer/Binary/.coq-native/NCoq_Numbers_Integer_Binary_ZBinary.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/Binary/.coq-native/NCoq_Numbers_Integer_Binary_ZBinary.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/Binary/.coq-native/NCoq_Numbers_Integer_Binary_ZBinary.cmxs
|
||||
|
|
@ -2334,20 +2253,6 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/NatPairs/.coq-
|
|||
lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.glob
|
||||
lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.v
|
||||
lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSig.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSig.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSig.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSig.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSigZAxioms.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSigZAxioms.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSigZAxioms.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Integer/SpecViaZ/.coq-native/NCoq_Numbers_Integer_SpecViaZ_ZSigZAxioms.o
|
||||
lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.glob
|
||||
lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.v
|
||||
lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.vo
|
||||
lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.glob
|
||||
lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
|
||||
lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo
|
||||
lib/coq/theories/Numbers/NaryFunctions.glob
|
||||
lib/coq/theories/Numbers/NaryFunctions.v
|
||||
lib/coq/theories/Numbers/NaryFunctions.vo
|
||||
|
|
@ -2603,34 +2508,6 @@ lib/coq/theories/Numbers/Natural/Abstract/NStrongRec.vo
|
|||
lib/coq/theories/Numbers/Natural/Abstract/NSub.glob
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NSub.v
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NSub.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_BigN.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_BigN.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_BigN.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_BigN.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake_gen.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake_gen.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake_gen.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_NMake_gen.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_Nbasic.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_Nbasic.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_Nbasic.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/BigN/.coq-native/NCoq_Numbers_Natural_BigN_Nbasic.o
|
||||
lib/coq/theories/Numbers/Natural/BigN/BigN.glob
|
||||
lib/coq/theories/Numbers/Natural/BigN/BigN.v
|
||||
lib/coq/theories/Numbers/Natural/BigN/BigN.vo
|
||||
lib/coq/theories/Numbers/Natural/BigN/NMake.glob
|
||||
lib/coq/theories/Numbers/Natural/BigN/NMake.v
|
||||
lib/coq/theories/Numbers/Natural/BigN/NMake.vo
|
||||
lib/coq/theories/Numbers/Natural/BigN/NMake_gen.glob
|
||||
lib/coq/theories/Numbers/Natural/BigN/NMake_gen.v
|
||||
lib/coq/theories/Numbers/Natural/BigN/NMake_gen.vo
|
||||
lib/coq/theories/Numbers/Natural/BigN/Nbasic.glob
|
||||
lib/coq/theories/Numbers/Natural/BigN/Nbasic.v
|
||||
lib/coq/theories/Numbers/Natural/BigN/Nbasic.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Natural/Binary/.coq-native/NCoq_Numbers_Natural_Binary_NBinary.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/Binary/.coq-native/NCoq_Numbers_Natural_Binary_NBinary.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/Binary/.coq-native/NCoq_Numbers_Natural_Binary_NBinary.cmxs
|
||||
|
|
@ -2645,44 +2522,9 @@ ${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/Peano/.coq-nat
|
|||
lib/coq/theories/Numbers/Natural/Peano/NPeano.glob
|
||||
lib/coq/theories/Numbers/Natural/Peano/NPeano.v
|
||||
lib/coq/theories/Numbers/Natural/Peano/NPeano.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSig.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSig.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSig.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSig.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSigNAxioms.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSigNAxioms.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSigNAxioms.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Natural/SpecViaZ/.coq-native/NCoq_Numbers_Natural_SpecViaZ_NSigNAxioms.o
|
||||
lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.glob
|
||||
lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.v
|
||||
lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.vo
|
||||
lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.glob
|
||||
lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
|
||||
lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo
|
||||
lib/coq/theories/Numbers/NumPrelude.glob
|
||||
lib/coq/theories/Numbers/NumPrelude.v
|
||||
lib/coq/theories/Numbers/NumPrelude.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_BigQ.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_BigQ.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_BigQ.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_BigQ.o
|
||||
${PLIST.native}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_QMake.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_QMake.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_QMake.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/BigQ/.coq-native/NCoq_Numbers_Rational_BigQ_QMake.o
|
||||
lib/coq/theories/Numbers/Rational/BigQ/BigQ.glob
|
||||
lib/coq/theories/Numbers/Rational/BigQ/BigQ.v
|
||||
lib/coq/theories/Numbers/Rational/BigQ/BigQ.vo
|
||||
lib/coq/theories/Numbers/Rational/BigQ/QMake.glob
|
||||
lib/coq/theories/Numbers/Rational/BigQ/QMake.v
|
||||
lib/coq/theories/Numbers/Rational/BigQ/QMake.vo
|
||||
${PLIST.native}lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native/NCoq_Numbers_Rational_SpecViaQ_QSig.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native/NCoq_Numbers_Rational_SpecViaQ_QSig.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native/NCoq_Numbers_Rational_SpecViaQ_QSig.cmxs
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/Numbers/Rational/SpecViaQ/.coq-native/NCoq_Numbers_Rational_SpecViaQ_QSig.o
|
||||
lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.glob
|
||||
lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.v
|
||||
lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.vo
|
||||
${PLIST.native}lib/coq/theories/PArith/.coq-native/NCoq_PArith_BinPos.cmi
|
||||
${PLIST.native}${PLIST.ocaml-opt}lib/coq/theories/PArith/.coq-native/NCoq_PArith_BinPos.cmx
|
||||
${PLIST.native}${PLIST.natdynlink}lib/coq/theories/PArith/.coq-native/NCoq_PArith_BinPos.cmxs
|
||||
|
|
@ -3999,41 +3841,46 @@ 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/CoqMakefile.in
|
||||
lib/coq/tools/TimeFileMaker.py
|
||||
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/class.cmi
|
||||
lib/coq/toplevel/classes.cmi
|
||||
lib/coq/toplevel/command.cmi
|
||||
lib/coq/tools/make-both-single-timing-files.py
|
||||
lib/coq/tools/make-both-time-files.py
|
||||
lib/coq/tools/make-one-time-file.py
|
||||
lib/coq/toplevel/coqinit.cmi
|
||||
lib/coq/toplevel/coqloop.cmi
|
||||
lib/coq/toplevel/coqtop.cmi
|
||||
lib/coq/toplevel/discharge.cmi
|
||||
lib/coq/toplevel/explainErr.cmi
|
||||
lib/coq/toplevel/himsg.cmi
|
||||
lib/coq/toplevel/ind_tables.cmi
|
||||
lib/coq/toplevel/indschemes.cmi
|
||||
lib/coq/toplevel/locality.cmi
|
||||
lib/coq/toplevel/metasyntax.cmi
|
||||
lib/coq/toplevel/mltop.cmi
|
||||
lib/coq/toplevel/obligations.cmi
|
||||
lib/coq/toplevel/record.cmi
|
||||
lib/coq/toplevel/search.cmi
|
||||
${PLIST.ocaml-opt}lib/coq/toplevel/toplevel.a
|
||||
lib/coq/toplevel/toplevel.cma
|
||||
${PLIST.ocaml-opt}lib/coq/toplevel/toplevel.cmxa
|
||||
lib/coq/toplevel/usage.cmi
|
||||
lib/coq/toplevel/vernac.cmi
|
||||
lib/coq/toplevel/vernacentries.cmi
|
||||
lib/coq/toplevel/vernacinterp.cmi
|
||||
${PLIST.ocaml-opt}${PLIST.coqide}lib/coq/toploop/coqidetop.cma
|
||||
lib/coq/vernac/assumptions.cmi
|
||||
lib/coq/vernac/auto_ind_decl.cmi
|
||||
lib/coq/vernac/class.cmi
|
||||
lib/coq/vernac/classes.cmi
|
||||
lib/coq/vernac/command.cmi
|
||||
lib/coq/vernac/declareDef.cmi
|
||||
lib/coq/vernac/discharge.cmi
|
||||
lib/coq/vernac/explainErr.cmi
|
||||
lib/coq/vernac/himsg.cmi
|
||||
lib/coq/vernac/indschemes.cmi
|
||||
lib/coq/vernac/lemmas.cmi
|
||||
lib/coq/vernac/locality.cmi
|
||||
lib/coq/vernac/metasyntax.cmi
|
||||
lib/coq/vernac/mltop.cmi
|
||||
lib/coq/vernac/obligations.cmi
|
||||
lib/coq/vernac/record.cmi
|
||||
lib/coq/vernac/search.cmi
|
||||
lib/coq/vernac/topfmt.cmi
|
||||
${PLIST.ocaml-opt}lib/coq/vernac/vernac.a
|
||||
${PLIST.ocaml-opt}lib/coq/vernac/vernac.cmxa
|
||||
lib/coq/vernac/vernacentries.cmi
|
||||
lib/coq/vernac/vernacinterp.cmi
|
||||
lib/coq/vernac/vernacprop.cmi
|
||||
${PLIST.natdynlink}${PLIST.coqide}lib/coq/toploop/coqidetop.cmxs
|
||||
${PLIST.ocaml-opt}lib/coq/toploop/proofworkertop.cma
|
||||
${PLIST.natdynlink}lib/coq/toploop/proofworkertop.cmxs
|
||||
${PLIST.ocaml-opt}lib/coq/toploop/queryworkertop.cma
|
||||
${PLIST.natdynlink}lib/coq/toploop/queryworkertop.cmxs
|
||||
${PLIST.ocaml-opt}lib/coq/toploop/tacworkertop.cma
|
||||
${PLIST.natdynlink}lib/coq/toploop/tacworkertop.cmxs
|
||||
man/man1/coq-tex.1
|
||||
man/man1/coq_makefile.1
|
||||
|
|
@ -4048,11 +3895,11 @@ man/man1/coqtop.byte.1
|
|||
man/man1/coqtop.opt.1
|
||||
man/man1/coqwc.1
|
||||
man/man1/gallina.1
|
||||
share/coq/coq-ssreflect.lang
|
||||
share/coq/coq.lang
|
||||
share/coq/coq.png
|
||||
share/coq/coq_style.xml
|
||||
share/doc/coq/FAQ-CoqIde
|
||||
${PLIST.coqide}share/coq/coq-ssreflect.lang
|
||||
${PLIST.coqide}share/coq/coq.lang
|
||||
${PLIST.coqide}share/coq/coq.png
|
||||
${PLIST.coqide}share/coq/coq_style.xml
|
||||
${PLIST.coqide}share/doc/coq/FAQ-CoqIde
|
||||
${PLIST.doc}share/doc/coq/LICENSE.doc
|
||||
${PLIST.doc}share/doc/coq/html/RecTutorial.html
|
||||
${PLIST.doc}share/doc/coq/html/Tutorial.html
|
||||
|
|
|
|||
|
|
@ -1,8 +1,9 @@
|
|||
$NetBSD: distinfo,v 1.27 2017/09/08 17:19:01 jaapb Exp $
|
||||
$NetBSD: distinfo,v 1.28 2017/11/03 11:20:28 jaapb Exp $
|
||||
|
||||
SHA1 (coq-8.6.1.tar.gz) = 5dbaf1230c297d7c11c8715c012300a51ad80f9a
|
||||
RMD160 (coq-8.6.1.tar.gz) = 822b0061a99de144881b1f1166eef9e92d26de7f
|
||||
SHA512 (coq-8.6.1.tar.gz) = 814ab76a06ca15f927081428da74add4bc67290199fa011853b9c68a00cdefaf813b10fbac18a434f4504fce8f2173eb544080bf6f50d62caa41bb8724b13083
|
||||
Size (coq-8.6.1.tar.gz) = 5588811 bytes
|
||||
SHA1 (patch-Makefile.common) = 79b02edff66ddcfb267816b0031c724620e67a13
|
||||
SHA1 (coq-8.7.0.tar.gz) = b539e0ff6f2a6dd31bbe8856db152705f9a22a01
|
||||
RMD160 (coq-8.7.0.tar.gz) = 7e752473b27a2d1a0f95ea3eb258ffba5a5a8d4f
|
||||
SHA512 (coq-8.7.0.tar.gz) = c806881d1ab823d9c2d748aa2d7fd3faaa0f6395536942ad214c68658b2688e6c57941947a440ddb69bf1436249067eefd866ecb1d9e4c5e774e3218c80a6fc2
|
||||
Size (coq-8.7.0.tar.gz) = 5629204 bytes
|
||||
SHA1 (patch-Makefile.common) = d84cb2a94227e163855f35abebe71f4ec51839fc
|
||||
SHA1 (patch-configure.ml) = 8e48a65709234281e3898ebae9041dfc04c7fe7b
|
||||
SHA1 (patch-ide_ideutils.ml) = 7fd59bcfc0cf4f65fd7f4e5a0ec95cb694df8417
|
||||
|
|
|
|||
|
|
@ -1,13 +1,15 @@
|
|||
$NetBSD: patch-Makefile.common,v 1.3 2016/12/30 13:23:06 jaapb Exp $
|
||||
$NetBSD: patch-Makefile.common,v 1.4 2017/11/03 11:20:28 jaapb Exp $
|
||||
|
||||
Use BSD_INSTALL_*
|
||||
--- Makefile.common.orig 2016-10-25 20:17:16.000000000 +0000
|
||||
--- Makefile.common.orig 2017-10-16 08:53:18.000000000 +0000
|
||||
+++ Makefile.common
|
||||
@@ -35,7 +35,7 @@ else
|
||||
@@ -69,8 +69,8 @@ DYNOBJ:=.cmo
|
||||
DYNLIB:=.cma
|
||||
endif
|
||||
|
||||
INSTALLBIN:=install
|
||||
-INSTALLLIB:=install -m 644
|
||||
-INSTALLBIN:=install
|
||||
-INSTALLLIB:=install -m 644
|
||||
+INSTALLBIN:=${BSD_INSTALL_PROGRAM}
|
||||
+INSTALLLIB:=${BSD_INSTALL_LIB}
|
||||
INSTALLSH:=./install.sh
|
||||
MKDIR:=install -d
|
||||
|
|
|
|||
14
lang/coq/patches/patch-ide_ideutils.ml
Normal file
14
lang/coq/patches/patch-ide_ideutils.ml
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
$NetBSD: patch-ide_ideutils.ml,v 1.1 2017/11/03 11:20:28 jaapb Exp $
|
||||
|
||||
For compilation with lablgtk 2.18.6
|
||||
--- ide/ideutils.ml.orig 2017-10-16 08:53:18.000000000 +0000
|
||||
+++ ide/ideutils.ml
|
||||
@@ -373,7 +373,7 @@ let io_read_all chan =
|
||||
Buffer.clear read_buffer;
|
||||
let read_once () =
|
||||
(* XXX: Glib.Io must be converted to bytes / -safe-string upstream *)
|
||||
- let len = Glib.Io.read_chars ~buf:(Bytes.unsafe_to_string read_string) ~pos:0 ~len:maxread chan in
|
||||
+ let len = Glib.Io.read_chars ~buf:read_string ~pos:0 ~len:maxread chan in
|
||||
Buffer.add_subbytes read_buffer read_string 0 len
|
||||
in
|
||||
begin
|
||||
Loading…
Reference in a new issue