mirror of
https://git.freebsd.org/ports.git
synced 2025-07-18 17:59:20 -04:00
Update to 8.6. Fix PORTEPOCH accidentally removed in the previous commit.
This commit is contained in:
Hiroki Sato
parent
42182c8c6e
commit
bb3308956b
Notes:
svn2git
2021-03-31 03:12:20 +00:00
svn path=/head/; revision=430173
6 changed files with 152 additions and 158 deletions
|
|
@ -1,7 +1,8 @@
|
|||
# $FreeBSD$
|
||||
|
||||
PORTNAME= coq
|
||||
PORTVERSION= 8.5
|
||||
PORTVERSION= 8.6
|
||||
PORTEPOCH= 3
|
||||
CATEGORIES= math
|
||||
MASTER_SITES= http://coq.inria.fr/distrib/V${PORTVERSION}/files/ \
|
||||
ftp://ftp.stack.nl/pub/users/johans/coq/
|
||||
|
|
@ -17,7 +18,6 @@ BUILD_DEPENDS= camlp5:devel/ocaml-camlp5 \
|
|||
LIB_DEPENDS= libfontconfig.so:x11-fonts/fontconfig \
|
||||
libfreetype.so:print/freetype2
|
||||
|
||||
COQVERSION= ${PORTVERSION:R}pl${PORTVERSION:E}
|
||||
USES= gmake gettext-runtime
|
||||
USE_EMACS= yes
|
||||
USE_GNOME= atk cairo gdkpixbuf2 glib20 gtk20 gtksourceview2 pango
|
||||
|
|
@ -28,8 +28,7 @@ CONFIGURE_ARGS= -prefix ${PREFIX} \
|
|||
-mandir ${PREFIX}/man \
|
||||
-emacslib ${PREFIX}/share/emacs/site-lisp/coq \
|
||||
-usecamlp5 \
|
||||
-byteonly \
|
||||
-makecmd ${MAKE_CMD}
|
||||
-byteonly
|
||||
MAKE_ENV= VERBOSE=1
|
||||
ALL_TARGET= world
|
||||
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
TIMESTAMP = 1483174912
|
||||
SHA256 (coq-8.5.tar.gz) = 89a92fb8b91e7cb0797d41c87cd13e4b63bee76c32a6dcc3d7c8055ca6a9ae3d
|
||||
SIZE (coq-8.5.tar.gz) = 5346653
|
||||
TIMESTAMP = 1483223265
|
||||
SHA256 (coq-8.6.tar.gz) = 6e3c3cf5c8e2b0b760dc52738e2e849f3a8c630869659ecc0cf41413fcee81df
|
||||
SIZE (coq-8.6.tar.gz) = 5538848
|
||||
|
|
|
|||
|
|
@ -1,29 +1,11 @@
|
|||
--- Makefile.build.orig 2016-01-20 16:52:18 UTC
|
||||
--- Makefile.build.orig 2016-12-08 15:13:52 UTC
|
||||
+++ Makefile.build
|
||||
@@ -56,7 +56,7 @@ CURDEPS:=$(addsuffix .d, $(CURFILES))
|
||||
@@ -101,7 +101,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMEC
|
||||
# TIME="%C (%U user, %S sys, %e total, %M maxres)"
|
||||
|
||||
# Variables meant to be modifiable via the command-line of make
|
||||
|
||||
-VERBOSE=
|
||||
+VERBOSE=1
|
||||
NO_RECOMPILE_ML4=
|
||||
NO_RECALC_DEPS=
|
||||
READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary
|
||||
@@ -82,7 +82,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U m
|
||||
TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
|
||||
|
||||
COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE)
|
||||
COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
|
||||
-BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
|
||||
+BOOTCOQC=$(TIMER) env CAML_LD_LIBRARY_PATH=$${PWD}/kernel/byterun $(COQTOPEXE) -boot $(COQOPTS) -compile
|
||||
|
||||
# The SHOW and HIDE variables control whether make will echo complete commands
|
||||
# or only abbreviated versions.
|
||||
@@ -704,7 +704,7 @@ install-doc-no:
|
||||
.PHONY: install install-doc-all install-doc-no
|
||||
|
||||
#These variables are intended to be set by the caller to make
|
||||
-#COQINSTALLPREFIX=
|
||||
+COQINSTALLPREFIX=${DESTDIR}
|
||||
#OLDROOT=
|
||||
|
||||
# Can be changed for a local installation (to make packages).
|
||||
LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
|
||||
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
|
||||
|
|
|
|||
11
math/coq/files/patch-Makefile.install
Normal file
11
math/coq/files/patch-Makefile.install
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
--- Makefile.install.orig 2016-12-08 15:13:52 UTC
|
||||
+++ Makefile.install
|
||||
@@ -29,7 +29,7 @@ install-doc-no:
|
||||
.PHONY: install install-doc-all install-doc-no
|
||||
|
||||
#These variables are intended to be set by the caller to make
|
||||
-#COQINSTALLPREFIX=
|
||||
+COQINSTALLPREFIX=${DESTDIR}
|
||||
#OLDROOT=
|
||||
|
||||
# Can be changed for a local installation (to make packages).
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
--- configure.ml.orig 2016-01-20 16:52:18 UTC
|
||||
+++ configure.ml
|
||||
@@ -843,7 +843,7 @@ let strip =
|
||||
(** * md5sum command *)
|
||||
|
||||
let md5sum =
|
||||
- if arch = "Darwin" then "md5 -q" else "md5sum"
|
||||
+ if arch = "FreeBSD" then "md5 -q" else "md5sum"
|
||||
|
||||
|
||||
(** * Documentation : do we have latex, hevea, ... *)
|
||||
|
|
@ -11,8 +11,22 @@ bin/coqtop.byte
|
|||
bin/coqwc
|
||||
bin/coqworkmgr
|
||||
bin/gallina
|
||||
lib/coq/META
|
||||
lib/coq/config/coq_config.cmi
|
||||
lib/coq/dllcoqrun.so
|
||||
lib/coq/engine/engine.cma
|
||||
lib/coq/engine/evarutil.cmi
|
||||
lib/coq/engine/evd.cmi
|
||||
lib/coq/engine/ftactic.cmi
|
||||
lib/coq/engine/geninterp.cmi
|
||||
lib/coq/engine/logic_monad.cmi
|
||||
lib/coq/engine/namegen.cmi
|
||||
lib/coq/engine/proofview.cmi
|
||||
lib/coq/engine/proofview_monad.cmi
|
||||
lib/coq/engine/sigma.cmi
|
||||
lib/coq/engine/termops.cmi
|
||||
lib/coq/engine/uState.cmi
|
||||
lib/coq/grammar/compat5.cmo
|
||||
lib/coq/grammar/grammar.cma
|
||||
lib/coq/grammar/q_util.cmi
|
||||
%%IDE%%lib/coq/ide/config_lexer.cmi
|
||||
|
|
@ -31,7 +45,9 @@ lib/coq/grammar/q_util.cmi
|
|||
%%IDE%%lib/coq/ide/nanoPG.cmi
|
||||
%%IDE%%lib/coq/ide/preferences.cmi
|
||||
%%IDE%%lib/coq/ide/project_file.cmi
|
||||
%%IDE%%lib/coq/ide/richprinter.cmi
|
||||
%%IDE%%lib/coq/ide/sentence.cmi
|
||||
%%IDE%%lib/coq/ide/serialize.cmi
|
||||
%%IDE%%lib/coq/ide/session.cmi
|
||||
%%IDE%%lib/coq/ide/tags.cmi
|
||||
%%IDE%%lib/coq/ide/utf8_convert.cmi
|
||||
|
|
@ -52,6 +68,9 @@ lib/coq/grammar/q_util.cmi
|
|||
%%IDE%%lib/coq/ide/wg_ProofView.cmi
|
||||
%%IDE%%lib/coq/ide/wg_ScriptView.cmi
|
||||
%%IDE%%lib/coq/ide/wg_Segment.cmi
|
||||
%%IDE%%lib/coq/ide/xml_lexer.cmi
|
||||
%%IDE%%lib/coq/ide/xml_parser.cmi
|
||||
%%IDE%%lib/coq/ide/xml_printer.cmi
|
||||
%%IDE%%lib/coq/ide/xmlprotocol.cmi
|
||||
lib/coq/interp/constrarg.cmi
|
||||
lib/coq/interp/constrexpr_ops.cmi
|
||||
|
|
@ -83,10 +102,10 @@ lib/coq/intf/notation_term.cmi
|
|||
lib/coq/intf/pattern.cmi
|
||||
lib/coq/intf/tacexpr.cmi
|
||||
lib/coq/intf/vernacexpr.cmi
|
||||
lib/coq/kernel/cClosure.cmi
|
||||
lib/coq/kernel/cbytecodes.cmi
|
||||
lib/coq/kernel/cbytegen.cmi
|
||||
lib/coq/kernel/cemitcodes.cmi
|
||||
lib/coq/kernel/closure.cmi
|
||||
lib/coq/kernel/constr.cmi
|
||||
lib/coq/kernel/context.cmi
|
||||
lib/coq/kernel/conv_oracle.cmi
|
||||
|
|
@ -126,6 +145,7 @@ lib/coq/kernel/term.cmi
|
|||
lib/coq/kernel/term_typing.cmi
|
||||
lib/coq/kernel/type_errors.cmi
|
||||
lib/coq/kernel/typeops.cmi
|
||||
lib/coq/kernel/uGraph.cmi
|
||||
lib/coq/kernel/uint31.cmi
|
||||
lib/coq/kernel/univ.cmi
|
||||
lib/coq/kernel/vars.cmi
|
||||
|
|
@ -135,6 +155,8 @@ lib/coq/lib/aux_file.cmi
|
|||
lib/coq/lib/backtrace.cmi
|
||||
lib/coq/lib/bigint.cmi
|
||||
lib/coq/lib/cArray.cmi
|
||||
lib/coq/lib/cEphemeron.cmi
|
||||
lib/coq/lib/cErrors.cmi
|
||||
lib/coq/lib/cList.cmi
|
||||
lib/coq/lib/cMap.cmi
|
||||
lib/coq/lib/cObj.cmi
|
||||
|
|
@ -144,14 +166,13 @@ lib/coq/lib/cStack.cmi
|
|||
lib/coq/lib/cString.cmi
|
||||
lib/coq/lib/cThread.cmi
|
||||
lib/coq/lib/cUnix.cmi
|
||||
lib/coq/lib/cWarnings.cmi
|
||||
lib/coq/lib/canary.cmi
|
||||
lib/coq/lib/clib.cma
|
||||
lib/coq/lib/control.cmi
|
||||
lib/coq/lib/deque.cmi
|
||||
lib/coq/lib/dyn.cmi
|
||||
lib/coq/lib/envars.cmi
|
||||
lib/coq/lib/ephemeron.cmi
|
||||
lib/coq/lib/errors.cmi
|
||||
lib/coq/lib/exninfo.cmi
|
||||
lib/coq/lib/explore.cmi
|
||||
lib/coq/lib/feedback.cmi
|
||||
|
|
@ -167,6 +188,7 @@ lib/coq/lib/iStream.cmi
|
|||
lib/coq/lib/int.cmi
|
||||
lib/coq/lib/lib.cma
|
||||
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
|
||||
|
|
@ -178,7 +200,6 @@ lib/coq/lib/remoteCounter.cmi
|
|||
lib/coq/lib/richpp.cmi
|
||||
lib/coq/lib/rtree.cmi
|
||||
lib/coq/lib/segmenttree.cmi
|
||||
lib/coq/lib/serialize.cmi
|
||||
lib/coq/lib/spawn.cmi
|
||||
lib/coq/lib/stateid.cmi
|
||||
lib/coq/lib/store.cmi
|
||||
|
|
@ -190,9 +211,6 @@ lib/coq/lib/unicodetable.cmi
|
|||
lib/coq/lib/unionfind.cmi
|
||||
lib/coq/lib/util.cmi
|
||||
lib/coq/lib/xml_datatype.cmi
|
||||
lib/coq/lib/xml_lexer.cmi
|
||||
lib/coq/lib/xml_parser.cmi
|
||||
lib/coq/lib/xml_printer.cmi
|
||||
lib/coq/library/declare.cmi
|
||||
lib/coq/library/declaremods.cmi
|
||||
lib/coq/library/decls.cmi
|
||||
|
|
@ -215,17 +233,39 @@ 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
|
||||
lib/coq/ltac/ltac.cma
|
||||
lib/coq/ltac/profile_ltac.cmi
|
||||
lib/coq/ltac/profile_ltac_tactics.cmi
|
||||
lib/coq/ltac/rewrite.cmi
|
||||
lib/coq/ltac/taccoerce.cmi
|
||||
lib/coq/ltac/tacentries.cmi
|
||||
lib/coq/ltac/tacenv.cmi
|
||||
lib/coq/ltac/tacintern.cmi
|
||||
lib/coq/ltac/tacinterp.cmi
|
||||
lib/coq/ltac/tacsubst.cmi
|
||||
lib/coq/ltac/tactic_debug.cmi
|
||||
lib/coq/ltac/tactic_option.cmi
|
||||
lib/coq/ltac/tauto.cmi
|
||||
lib/coq/parsing/cLexer.cmi
|
||||
lib/coq/parsing/compat.cmi
|
||||
lib/coq/parsing/egramcoq.cmi
|
||||
lib/coq/parsing/egramml.cmi
|
||||
lib/coq/parsing/g_constr.cmi
|
||||
lib/coq/parsing/g_ltac.cmi
|
||||
lib/coq/parsing/g_prim.cmi
|
||||
lib/coq/parsing/g_proofs.cmi
|
||||
lib/coq/parsing/g_tactic.cmi
|
||||
lib/coq/parsing/g_vernac.cmi
|
||||
lib/coq/parsing/highparsing.cma
|
||||
lib/coq/parsing/lexer.cmi
|
||||
lib/coq/parsing/parsing.cma
|
||||
lib/coq/parsing/pcoq.cmi
|
||||
lib/coq/parsing/tok.cmi
|
||||
|
|
@ -244,23 +284,19 @@ lib/coq/plugins/btauto/Btauto.vo
|
|||
lib/coq/plugins/btauto/Reflect.glob
|
||||
lib/coq/plugins/btauto/Reflect.v
|
||||
lib/coq/plugins/btauto/Reflect.vo
|
||||
lib/coq/plugins/btauto/btauto_plugin.cma
|
||||
lib/coq/plugins/btauto/btauto_plugin_mod.cmi
|
||||
lib/coq/plugins/btauto/g_btauto.cmi
|
||||
lib/coq/plugins/btauto/refl_btauto.cmi
|
||||
lib/coq/plugins/cc/cc_plugin.cma
|
||||
lib/coq/plugins/cc/cc_plugin_mod.cmi
|
||||
lib/coq/plugins/btauto/btauto_plugin.cmi
|
||||
lib/coq/plugins/btauto/btauto_plugin.cmo
|
||||
lib/coq/plugins/cc/cc_plugin.cmi
|
||||
lib/coq/plugins/cc/cc_plugin.cmo
|
||||
lib/coq/plugins/cc/ccalgo.cmi
|
||||
lib/coq/plugins/cc/ccproof.cmi
|
||||
lib/coq/plugins/cc/cctac.cmi
|
||||
lib/coq/plugins/cc/g_congruence.cmi
|
||||
lib/coq/plugins/decl_mode/decl_expr.cmi
|
||||
lib/coq/plugins/decl_mode/decl_interp.cmi
|
||||
lib/coq/plugins/decl_mode/decl_mode.cmi
|
||||
lib/coq/plugins/decl_mode/decl_mode_plugin.cma
|
||||
lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi
|
||||
lib/coq/plugins/decl_mode/decl_mode_plugin.cmi
|
||||
lib/coq/plugins/decl_mode/decl_mode_plugin.cmo
|
||||
lib/coq/plugins/decl_mode/decl_proof_instr.cmi
|
||||
lib/coq/plugins/decl_mode/g_decl_mode.cmi
|
||||
lib/coq/plugins/decl_mode/ppdecl_proof.cmi
|
||||
lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmi
|
||||
lib/coq/plugins/derive/.coq-native/NCoq_derive_Derive.cmo
|
||||
|
|
@ -268,8 +304,8 @@ lib/coq/plugins/derive/Derive.glob
|
|||
lib/coq/plugins/derive/Derive.v
|
||||
lib/coq/plugins/derive/Derive.vo
|
||||
lib/coq/plugins/derive/derive.cmi
|
||||
lib/coq/plugins/derive/derive_plugin.cma
|
||||
lib/coq/plugins/derive/g_derive.cmi
|
||||
lib/coq/plugins/derive/derive_plugin.cmi
|
||||
lib/coq/plugins/derive/derive_plugin.cmo
|
||||
lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmi
|
||||
lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellBasic.cmo
|
||||
lib/coq/plugins/extraction/.coq-native/NCoq_extraction_ExtrHaskellNatInt.cmi
|
||||
|
|
@ -353,9 +389,8 @@ lib/coq/plugins/extraction/ExtrOcamlZInt.vo
|
|||
lib/coq/plugins/extraction/common.cmi
|
||||
lib/coq/plugins/extraction/extract_env.cmi
|
||||
lib/coq/plugins/extraction/extraction.cmi
|
||||
lib/coq/plugins/extraction/extraction_plugin.cma
|
||||
lib/coq/plugins/extraction/extraction_plugin_mod.cmi
|
||||
lib/coq/plugins/extraction/g_extraction.cmi
|
||||
lib/coq/plugins/extraction/extraction_plugin.cmi
|
||||
lib/coq/plugins/extraction/extraction_plugin.cmo
|
||||
lib/coq/plugins/extraction/haskell.cmi
|
||||
lib/coq/plugins/extraction/json.cmi
|
||||
lib/coq/plugins/extraction/miniml.cmi
|
||||
|
|
@ -365,10 +400,9 @@ lib/coq/plugins/extraction/ocaml.cmi
|
|||
lib/coq/plugins/extraction/scheme.cmi
|
||||
lib/coq/plugins/extraction/table.cmi
|
||||
lib/coq/plugins/firstorder/formula.cmi
|
||||
lib/coq/plugins/firstorder/g_ground.cmi
|
||||
lib/coq/plugins/firstorder/ground.cmi
|
||||
lib/coq/plugins/firstorder/ground_plugin.cma
|
||||
lib/coq/plugins/firstorder/ground_plugin_mod.cmi
|
||||
lib/coq/plugins/firstorder/ground_plugin.cmi
|
||||
lib/coq/plugins/firstorder/ground_plugin.cmo
|
||||
lib/coq/plugins/firstorder/instances.cmi
|
||||
lib/coq/plugins/firstorder/rules.cmi
|
||||
lib/coq/plugins/firstorder/sequent.cmi
|
||||
|
|
@ -383,11 +417,8 @@ lib/coq/plugins/fourier/Fourier.vo
|
|||
lib/coq/plugins/fourier/Fourier_util.glob
|
||||
lib/coq/plugins/fourier/Fourier_util.v
|
||||
lib/coq/plugins/fourier/Fourier_util.vo
|
||||
lib/coq/plugins/fourier/fourier.cmi
|
||||
lib/coq/plugins/fourier/fourierR.cmi
|
||||
lib/coq/plugins/fourier/fourier_plugin.cma
|
||||
lib/coq/plugins/fourier/fourier_plugin_mod.cmi
|
||||
lib/coq/plugins/fourier/g_fourier.cmi
|
||||
lib/coq/plugins/fourier/fourier_plugin.cmi
|
||||
lib/coq/plugins/fourier/fourier_plugin.cmo
|
||||
lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmi
|
||||
lib/coq/plugins/funind/.coq-native/NCoq_funind_Recdef.cmo
|
||||
lib/coq/plugins/funind/Recdef.glob
|
||||
|
|
@ -395,22 +426,23 @@ lib/coq/plugins/funind/Recdef.v
|
|||
lib/coq/plugins/funind/Recdef.vo
|
||||
lib/coq/plugins/funind/functional_principles_proofs.cmi
|
||||
lib/coq/plugins/funind/functional_principles_types.cmi
|
||||
lib/coq/plugins/funind/g_indfun.cmi
|
||||
lib/coq/plugins/funind/glob_term_to_relation.cmi
|
||||
lib/coq/plugins/funind/glob_termops.cmi
|
||||
lib/coq/plugins/funind/indfun.cmi
|
||||
lib/coq/plugins/funind/indfun_common.cmi
|
||||
lib/coq/plugins/funind/invfun.cmi
|
||||
lib/coq/plugins/funind/merge.cmi
|
||||
lib/coq/plugins/funind/recdef.cmi
|
||||
lib/coq/plugins/funind/recdef_plugin.cma
|
||||
lib/coq/plugins/funind/recdef_plugin_mod.cmi
|
||||
lib/coq/plugins/funind/recdef_plugin.cmi
|
||||
lib/coq/plugins/funind/recdef_plugin.cmo
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmi
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Env.cmo
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmi
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_EnvRing.cmo
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmi
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lia.cmo
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmi
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lqa.cmo
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmi
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Lra.cmo
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmi
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_OrderedRing.cmo
|
||||
lib/coq/plugins/micromega/.coq-native/NCoq_micromega_Psatz.cmi
|
||||
|
|
@ -440,6 +472,12 @@ lib/coq/plugins/micromega/EnvRing.vo
|
|||
lib/coq/plugins/micromega/Lia.glob
|
||||
lib/coq/plugins/micromega/Lia.v
|
||||
lib/coq/plugins/micromega/Lia.vo
|
||||
lib/coq/plugins/micromega/Lqa.glob
|
||||
lib/coq/plugins/micromega/Lqa.v
|
||||
lib/coq/plugins/micromega/Lqa.vo
|
||||
lib/coq/plugins/micromega/Lra.glob
|
||||
lib/coq/plugins/micromega/Lra.v
|
||||
lib/coq/plugins/micromega/Lra.vo
|
||||
lib/coq/plugins/micromega/OrderedRing.glob
|
||||
lib/coq/plugins/micromega/OrderedRing.v
|
||||
lib/coq/plugins/micromega/OrderedRing.vo
|
||||
|
|
@ -470,19 +508,11 @@ lib/coq/plugins/micromega/ZCoeff.vo
|
|||
lib/coq/plugins/micromega/ZMicromega.glob
|
||||
lib/coq/plugins/micromega/ZMicromega.v
|
||||
lib/coq/plugins/micromega/ZMicromega.vo
|
||||
lib/coq/plugins/micromega/certificate.cmi
|
||||
lib/coq/plugins/micromega/coq_micromega.cmi
|
||||
lib/coq/plugins/micromega/csdpcert
|
||||
lib/coq/plugins/micromega/g_micromega.cmi
|
||||
lib/coq/plugins/micromega/mfourier.cmi
|
||||
lib/coq/plugins/micromega/micromega.cmi
|
||||
lib/coq/plugins/micromega/micromega_plugin.cma
|
||||
lib/coq/plugins/micromega/micromega_plugin_mod.cmi
|
||||
lib/coq/plugins/micromega/mutils.cmi
|
||||
lib/coq/plugins/micromega/persistent_cache.cmi
|
||||
lib/coq/plugins/micromega/polynomial.cmi
|
||||
lib/coq/plugins/micromega/micromega_plugin.cmi
|
||||
lib/coq/plugins/micromega/micromega_plugin.cmo
|
||||
lib/coq/plugins/micromega/sos.cmi
|
||||
lib/coq/plugins/micromega/sos_types.cmi
|
||||
lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmi
|
||||
lib/coq/plugins/nsatz/.coq-native/NCoq_nsatz_Nsatz.cmo
|
||||
lib/coq/plugins/nsatz/Nsatz.glob
|
||||
|
|
@ -490,8 +520,8 @@ lib/coq/plugins/nsatz/Nsatz.v
|
|||
lib/coq/plugins/nsatz/Nsatz.vo
|
||||
lib/coq/plugins/nsatz/ideal.cmi
|
||||
lib/coq/plugins/nsatz/nsatz.cmi
|
||||
lib/coq/plugins/nsatz/nsatz_plugin.cma
|
||||
lib/coq/plugins/nsatz/nsatz_plugin_mod.cmi
|
||||
lib/coq/plugins/nsatz/nsatz_plugin.cmi
|
||||
lib/coq/plugins/nsatz/nsatz_plugin.cmo
|
||||
lib/coq/plugins/nsatz/polynom.cmi
|
||||
lib/coq/plugins/nsatz/utile.cmi
|
||||
lib/coq/plugins/omega/.coq-native/NCoq_omega_Omega.cmi
|
||||
|
|
@ -519,20 +549,15 @@ lib/coq/plugins/omega/OmegaTactic.vo
|
|||
lib/coq/plugins/omega/PreOmega.glob
|
||||
lib/coq/plugins/omega/PreOmega.v
|
||||
lib/coq/plugins/omega/PreOmega.vo
|
||||
lib/coq/plugins/omega/coq_omega.cmi
|
||||
lib/coq/plugins/omega/g_omega.cmi
|
||||
lib/coq/plugins/omega/omega.cmi
|
||||
lib/coq/plugins/omega/omega_plugin.cma
|
||||
lib/coq/plugins/omega/omega_plugin_mod.cmi
|
||||
lib/coq/plugins/omega/omega_plugin.cmi
|
||||
lib/coq/plugins/omega/omega_plugin.cmo
|
||||
lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmi
|
||||
lib/coq/plugins/quote/.coq-native/NCoq_quote_Quote.cmo
|
||||
lib/coq/plugins/quote/Quote.glob
|
||||
lib/coq/plugins/quote/Quote.v
|
||||
lib/coq/plugins/quote/Quote.vo
|
||||
lib/coq/plugins/quote/g_quote.cmi
|
||||
lib/coq/plugins/quote/quote.cmi
|
||||
lib/coq/plugins/quote/quote_plugin.cma
|
||||
lib/coq/plugins/quote/quote_plugin_mod.cmi
|
||||
lib/coq/plugins/quote/quote_plugin.cmi
|
||||
lib/coq/plugins/quote/quote_plugin.cmo
|
||||
lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmi
|
||||
lib/coq/plugins/romega/.coq-native/NCoq_romega_ROmega.cmo
|
||||
lib/coq/plugins/romega/.coq-native/NCoq_romega_ReflOmegaCore.cmi
|
||||
|
|
@ -544,10 +569,8 @@ lib/coq/plugins/romega/ReflOmegaCore.glob
|
|||
lib/coq/plugins/romega/ReflOmegaCore.v
|
||||
lib/coq/plugins/romega/ReflOmegaCore.vo
|
||||
lib/coq/plugins/romega/const_omega.cmi
|
||||
lib/coq/plugins/romega/g_romega.cmi
|
||||
lib/coq/plugins/romega/refl_omega.cmi
|
||||
lib/coq/plugins/romega/romega_plugin.cma
|
||||
lib/coq/plugins/romega/romega_plugin_mod.cmi
|
||||
lib/coq/plugins/romega/romega_plugin.cmi
|
||||
lib/coq/plugins/romega/romega_plugin.cmo
|
||||
lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmi
|
||||
lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Bintree.cmo
|
||||
lib/coq/plugins/rtauto/.coq-native/NCoq_rtauto_Rtauto.cmi
|
||||
|
|
@ -558,11 +581,10 @@ lib/coq/plugins/rtauto/Bintree.vo
|
|||
lib/coq/plugins/rtauto/Rtauto.glob
|
||||
lib/coq/plugins/rtauto/Rtauto.v
|
||||
lib/coq/plugins/rtauto/Rtauto.vo
|
||||
lib/coq/plugins/rtauto/g_rtauto.cmi
|
||||
lib/coq/plugins/rtauto/proof_search.cmi
|
||||
lib/coq/plugins/rtauto/refl_tauto.cmi
|
||||
lib/coq/plugins/rtauto/rtauto_plugin.cma
|
||||
lib/coq/plugins/rtauto/rtauto_plugin_mod.cmi
|
||||
lib/coq/plugins/rtauto/rtauto_plugin.cmi
|
||||
lib/coq/plugins/rtauto/rtauto_plugin.cmo
|
||||
lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmi
|
||||
lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_Algebra_syntax.cmo
|
||||
lib/coq/plugins/setoid_ring/.coq-native/NCoq_setoid_ring_ArithRing.cmi
|
||||
|
|
@ -684,26 +706,29 @@ lib/coq/plugins/setoid_ring/ZArithRing.glob
|
|||
lib/coq/plugins/setoid_ring/ZArithRing.v
|
||||
lib/coq/plugins/setoid_ring/ZArithRing.vo
|
||||
lib/coq/plugins/setoid_ring/newring.cmi
|
||||
lib/coq/plugins/setoid_ring/newring_plugin.cma
|
||||
lib/coq/plugins/setoid_ring/newring_plugin_mod.cmi
|
||||
lib/coq/plugins/syntax/ascii_syntax.cmi
|
||||
lib/coq/plugins/syntax/ascii_syntax_plugin.cma
|
||||
lib/coq/plugins/syntax/ascii_syntax_plugin_mod.cmi
|
||||
lib/coq/plugins/syntax/nat_syntax.cmi
|
||||
lib/coq/plugins/syntax/nat_syntax_plugin.cma
|
||||
lib/coq/plugins/syntax/nat_syntax_plugin_mod.cmi
|
||||
lib/coq/plugins/syntax/numbers_syntax.cmi
|
||||
lib/coq/plugins/syntax/numbers_syntax_plugin.cma
|
||||
lib/coq/plugins/syntax/numbers_syntax_plugin_mod.cmi
|
||||
lib/coq/plugins/syntax/r_syntax.cmi
|
||||
lib/coq/plugins/syntax/r_syntax_plugin.cma
|
||||
lib/coq/plugins/syntax/r_syntax_plugin_mod.cmi
|
||||
lib/coq/plugins/syntax/string_syntax.cmi
|
||||
lib/coq/plugins/syntax/string_syntax_plugin.cma
|
||||
lib/coq/plugins/syntax/string_syntax_plugin_mod.cmi
|
||||
lib/coq/plugins/syntax/z_syntax.cmi
|
||||
lib/coq/plugins/syntax/z_syntax_plugin.cma
|
||||
lib/coq/plugins/syntax/z_syntax_plugin_mod.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
|
||||
lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmi
|
||||
lib/coq/plugins/ssrmatching/.coq-native/NCoq_ssrmatching_ssrmatching.cmo
|
||||
lib/coq/plugins/ssrmatching/ssrmatching.cmi
|
||||
lib/coq/plugins/ssrmatching/ssrmatching.glob
|
||||
lib/coq/plugins/ssrmatching/ssrmatching.v
|
||||
lib/coq/plugins/ssrmatching/ssrmatching.vo
|
||||
lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmi
|
||||
lib/coq/plugins/ssrmatching/ssrmatching_plugin.cmo
|
||||
lib/coq/plugins/syntax/ascii_syntax_plugin.cmi
|
||||
lib/coq/plugins/syntax/ascii_syntax_plugin.cmo
|
||||
lib/coq/plugins/syntax/nat_syntax_plugin.cmi
|
||||
lib/coq/plugins/syntax/nat_syntax_plugin.cmo
|
||||
lib/coq/plugins/syntax/numbers_syntax_plugin.cmi
|
||||
lib/coq/plugins/syntax/numbers_syntax_plugin.cmo
|
||||
lib/coq/plugins/syntax/r_syntax_plugin.cmi
|
||||
lib/coq/plugins/syntax/r_syntax_plugin.cmo
|
||||
lib/coq/plugins/syntax/string_syntax_plugin.cmi
|
||||
lib/coq/plugins/syntax/string_syntax_plugin.cmo
|
||||
lib/coq/plugins/syntax/z_syntax_plugin.cmi
|
||||
lib/coq/plugins/syntax/z_syntax_plugin.cmo
|
||||
lib/coq/pretyping/arguments_renaming.cmi
|
||||
lib/coq/pretyping/cases.cmi
|
||||
lib/coq/pretyping/cbv.cmi
|
||||
|
|
@ -712,16 +737,14 @@ lib/coq/pretyping/coercion.cmi
|
|||
lib/coq/pretyping/constr_matching.cmi
|
||||
lib/coq/pretyping/detyping.cmi
|
||||
lib/coq/pretyping/evarconv.cmi
|
||||
lib/coq/pretyping/evardefine.cmi
|
||||
lib/coq/pretyping/evarsolve.cmi
|
||||
lib/coq/pretyping/evarutil.cmi
|
||||
lib/coq/pretyping/evd.cmi
|
||||
lib/coq/pretyping/find_subterm.cmi
|
||||
lib/coq/pretyping/glob_ops.cmi
|
||||
lib/coq/pretyping/indrec.cmi
|
||||
lib/coq/pretyping/inductiveops.cmi
|
||||
lib/coq/pretyping/locusops.cmi
|
||||
lib/coq/pretyping/miscops.cmi
|
||||
lib/coq/pretyping/namegen.cmi
|
||||
lib/coq/pretyping/nativenorm.cmi
|
||||
lib/coq/pretyping/patternops.cmi
|
||||
lib/coq/pretyping/pretype_errors.cmi
|
||||
|
|
@ -733,7 +756,6 @@ lib/coq/pretyping/redops.cmi
|
|||
lib/coq/pretyping/reductionops.cmi
|
||||
lib/coq/pretyping/retyping.cmi
|
||||
lib/coq/pretyping/tacred.cmi
|
||||
lib/coq/pretyping/termops.cmi
|
||||
lib/coq/pretyping/typeclasses.cmi
|
||||
lib/coq/pretyping/typeclasses_errors.cmi
|
||||
lib/coq/pretyping/typing.cmi
|
||||
|
|
@ -754,34 +776,30 @@ lib/coq/printing/printer.cmi
|
|||
lib/coq/printing/printing.cma
|
||||
lib/coq/printing/printmod.cmi
|
||||
lib/coq/printing/printmodsig.cmi
|
||||
lib/coq/printing/richprinter.cmi
|
||||
lib/coq/proofs/clenv.cmi
|
||||
lib/coq/proofs/clenvtac.cmi
|
||||
lib/coq/proofs/evar_refiner.cmi
|
||||
lib/coq/proofs/goal.cmi
|
||||
lib/coq/proofs/logic.cmi
|
||||
lib/coq/proofs/logic_monad.cmi
|
||||
lib/coq/proofs/pfedit.cmi
|
||||
lib/coq/proofs/proof.cmi
|
||||
lib/coq/proofs/proof_global.cmi
|
||||
lib/coq/proofs/proof_type.cmi
|
||||
lib/coq/proofs/proof_using.cmi
|
||||
lib/coq/proofs/proofs.cma
|
||||
lib/coq/proofs/proofview.cmi
|
||||
lib/coq/proofs/proofview_monad.cmi
|
||||
lib/coq/proofs/redexpr.cmi
|
||||
lib/coq/proofs/refine.cmi
|
||||
lib/coq/proofs/refiner.cmi
|
||||
lib/coq/proofs/tacmach.cmi
|
||||
lib/coq/proofs/tactic_debug.cmi
|
||||
lib/coq/stm/asyncTaskQueue.cmi
|
||||
lib/coq/stm/coqworkmgrApi.cmi
|
||||
lib/coq/stm/dag.cmi
|
||||
lib/coq/stm/lemmas.cmi
|
||||
lib/coq/stm/proofBlockDelimiter.cmi
|
||||
lib/coq/stm/spawned.cmi
|
||||
lib/coq/stm/stm.cma
|
||||
lib/coq/stm/stm.cmi
|
||||
lib/coq/stm/tQueue.cmi
|
||||
lib/coq/stm/texmacspp.cmi
|
||||
lib/coq/stm/vcs.cmi
|
||||
lib/coq/stm/vernac_classifier.cmi
|
||||
lib/coq/stm/vio_checking.cmi
|
||||
|
|
@ -791,7 +809,6 @@ lib/coq/tactics/autorewrite.cmi
|
|||
lib/coq/tactics/btermdn.cmi
|
||||
lib/coq/tactics/class_tactics.cmi
|
||||
lib/coq/tactics/contradiction.cmi
|
||||
lib/coq/tactics/coretactics.cmi
|
||||
lib/coq/tactics/dn.cmi
|
||||
lib/coq/tactics/dnet.cmi
|
||||
lib/coq/tactics/eauto.cmi
|
||||
|
|
@ -800,31 +817,14 @@ lib/coq/tactics/elimschemes.cmi
|
|||
lib/coq/tactics/eqdecide.cmi
|
||||
lib/coq/tactics/eqschemes.cmi
|
||||
lib/coq/tactics/equality.cmi
|
||||
lib/coq/tactics/evar_tactics.cmi
|
||||
lib/coq/tactics/extraargs.cmi
|
||||
lib/coq/tactics/extratactics.cmi
|
||||
lib/coq/tactics/ftactic.cmi
|
||||
lib/coq/tactics/g_class.cmi
|
||||
lib/coq/tactics/g_eqdecide.cmi
|
||||
lib/coq/tactics/g_rewrite.cmi
|
||||
lib/coq/tactics/geninterp.cmi
|
||||
lib/coq/tactics/hightactics.cma
|
||||
lib/coq/tactics/hints.cmi
|
||||
lib/coq/tactics/hipattern.cmi
|
||||
lib/coq/tactics/inv.cmi
|
||||
lib/coq/tactics/leminv.cmi
|
||||
lib/coq/tactics/rewrite.cmi
|
||||
lib/coq/tactics/taccoerce.cmi
|
||||
lib/coq/tactics/tacenv.cmi
|
||||
lib/coq/tactics/tacintern.cmi
|
||||
lib/coq/tactics/tacinterp.cmi
|
||||
lib/coq/tactics/tacsubst.cmi
|
||||
lib/coq/tactics/tactic_matching.cmi
|
||||
lib/coq/tactics/tactic_option.cmi
|
||||
lib/coq/tactics/tacticals.cmi
|
||||
lib/coq/tactics/tactics.cma
|
||||
lib/coq/tactics/tactics.cmi
|
||||
lib/coq/tactics/tauto.cmi
|
||||
lib/coq/tactics/term_dnet.cmi
|
||||
lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmi
|
||||
lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmo
|
||||
|
|
@ -1052,6 +1052,8 @@ lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmi
|
|||
lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq84.cmo
|
||||
lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmi
|
||||
lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq85.cmo
|
||||
lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmi
|
||||
lib/coq/theories/Compat/.coq-native/NCoq_Compat_Coq86.cmo
|
||||
lib/coq/theories/Compat/AdmitAxiom.glob
|
||||
lib/coq/theories/Compat/AdmitAxiom.v
|
||||
lib/coq/theories/Compat/AdmitAxiom.vo
|
||||
|
|
@ -1061,6 +1063,9 @@ lib/coq/theories/Compat/Coq84.vo
|
|||
lib/coq/theories/Compat/Coq85.glob
|
||||
lib/coq/theories/Compat/Coq85.v
|
||||
lib/coq/theories/Compat/Coq85.vo
|
||||
lib/coq/theories/Compat/Coq86.glob
|
||||
lib/coq/theories/Compat/Coq86.v
|
||||
lib/coq/theories/Compat/Coq86.vo
|
||||
lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmi
|
||||
lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapAVL.cmo
|
||||
lib/coq/theories/FSets/.coq-native/NCoq_FSets_FMapFacts.cmi
|
||||
|
|
@ -1184,6 +1189,8 @@ lib/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmi
|
|||
lib/coq/theories/Init/.coq-native/NCoq_Init_Specif.cmo
|
||||
lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmi
|
||||
lib/coq/theories/Init/.coq-native/NCoq_Init_Tactics.cmo
|
||||
lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmi
|
||||
lib/coq/theories/Init/.coq-native/NCoq_Init_Tauto.cmo
|
||||
lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmi
|
||||
lib/coq/theories/Init/.coq-native/NCoq_Init_Wf.cmo
|
||||
lib/coq/theories/Init/Datatypes.glob
|
||||
|
|
@ -1213,6 +1220,9 @@ lib/coq/theories/Init/Specif.vo
|
|||
lib/coq/theories/Init/Tactics.glob
|
||||
lib/coq/theories/Init/Tactics.v
|
||||
lib/coq/theories/Init/Tactics.vo
|
||||
lib/coq/theories/Init/Tauto.glob
|
||||
lib/coq/theories/Init/Tauto.v
|
||||
lib/coq/theories/Init/Tauto.vo
|
||||
lib/coq/theories/Init/Wf.glob
|
||||
lib/coq/theories/Init/Wf.v
|
||||
lib/coq/theories/Init/Wf.vo
|
||||
|
|
@ -2054,6 +2064,8 @@ lib/coq/theories/QArith/.coq-native/NCoq_QArith_QOrderedType.cmi
|
|||
lib/coq/theories/QArith/.coq-native/NCoq_QArith_QOrderedType.cmo
|
||||
lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmi
|
||||
lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qabs.cmo
|
||||
lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmi
|
||||
lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcabs.cmo
|
||||
lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmi
|
||||
lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qcanon.cmo
|
||||
lib/coq/theories/QArith/.coq-native/NCoq_QArith_Qfield.cmi
|
||||
|
|
@ -2082,6 +2094,9 @@ lib/coq/theories/QArith/QOrderedType.vo
|
|||
lib/coq/theories/QArith/Qabs.glob
|
||||
lib/coq/theories/QArith/Qabs.v
|
||||
lib/coq/theories/QArith/Qabs.vo
|
||||
lib/coq/theories/QArith/Qcabs.glob
|
||||
lib/coq/theories/QArith/Qcabs.v
|
||||
lib/coq/theories/QArith/Qcabs.vo
|
||||
lib/coq/theories/QArith/Qcanon.glob
|
||||
lib/coq/theories/QArith/Qcanon.v
|
||||
lib/coq/theories/QArith/Qcanon.vo
|
||||
|
|
@ -2911,12 +2926,10 @@ lib/coq/theories/ZArith/Zwf.vo
|
|||
lib/coq/theories/ZArith/auxiliary.glob
|
||||
lib/coq/theories/ZArith/auxiliary.v
|
||||
lib/coq/theories/ZArith/auxiliary.vo
|
||||
lib/coq/tools/compat5.cmo
|
||||
lib/coq/tools/coqdoc/coqdoc.css
|
||||
lib/coq/tools/coqdoc/coqdoc.sty
|
||||
lib/coq/toplevel/assumptions.cmi
|
||||
lib/coq/toplevel/auto_ind_decl.cmi
|
||||
lib/coq/toplevel/cerrors.cmi
|
||||
lib/coq/toplevel/class.cmi
|
||||
lib/coq/toplevel/classes.cmi
|
||||
lib/coq/toplevel/command.cmi
|
||||
|
|
@ -2924,7 +2937,7 @@ lib/coq/toplevel/coqinit.cmi
|
|||
lib/coq/toplevel/coqloop.cmi
|
||||
lib/coq/toplevel/coqtop.cmi
|
||||
lib/coq/toplevel/discharge.cmi
|
||||
lib/coq/toplevel/g_obligations.cmi
|
||||
lib/coq/toplevel/explainErr.cmi
|
||||
lib/coq/toplevel/himsg.cmi
|
||||
lib/coq/toplevel/ind_tables.cmi
|
||||
lib/coq/toplevel/indschemes.cmi
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue