mirror of
https://git.FreeBSD.org/ports.git
synced 2024-11-27 00:57:50 +00:00
- Update coq to 8.3
- Add a patch to fix threading issues Submitted by: AUGER Cedric <Cedric.Auger@lri.fr>
This commit is contained in:
Johan van Selst
parent
155dbbd53b
commit
51ccf06067
Notes:
svn2git
2021-03-31 03:12:20 +00:00
svn path=/head/; revision=264298
@ -6,7 +6,7 @@
|
||||
#
|
||||
|
||||
PORTNAME= coq
|
||||
DISTVERSION= 8.2pl1
|
||||
DISTVERSION= 8.3
|
||||
PORTEPOCH= 1
|
||||
CATEGORIES= math
|
||||
MASTER_SITES= http://coq.inria.fr/distrib/V${DISTVERSION}/files/ \
|
||||
@ -25,25 +25,21 @@ WITH_IDE= yes
|
||||
HAS_CONFIGURE= yes
|
||||
CONFIGURE_ARGS= --prefix ${PREFIX}
|
||||
CONFIGURE_ARGS+=--emacslib ${PREFIX}/share/emacs/site-lisp
|
||||
CONFIGURE_ARGS+=--reals all
|
||||
CONFIGURE_ARGS+=--opt
|
||||
|
||||
.ifdef NOPORTDOCS
|
||||
CONFIGURE_ARGS+=--with-doc none
|
||||
.else
|
||||
BUILD_DEPENDS+= hevea:${PORTSDIR}/textproc/hevea
|
||||
BUILD_DEPENDS+= hevea:${PORTSDIR}/textproc/hevea \
|
||||
latex:${PORTSDIR}/print/teTeX \
|
||||
${LOCALBASE}/share/texmf/tex/latex/ucs/utf8x.def:${PORTSDIR}/print/latex-ucs
|
||||
PORTDOCS= *
|
||||
.endif
|
||||
|
||||
.include <bsd.port.pre.mk>
|
||||
|
||||
.if ${ARCH} == "ia64"
|
||||
BROKEN= OCaml bug prevents compilation
|
||||
.endif
|
||||
|
||||
MAN1= coq-interface.1 coq-tex.1 coq_makefile.1 coqc.1 coqdep.1 coqdoc.1 \
|
||||
coqmktop.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqwc.1 gallina.1 \
|
||||
coq-parser.1
|
||||
MAN1= coq-tex.1 coq_makefile.1 coqc.1 coqchk.1 coqdep.1 coqdoc.1 \
|
||||
coqmktop.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqwc.1 gallina.1
|
||||
|
||||
.if defined(WITH_IDE) || exists(${LOCALBASE}/bin/lablgtk2)
|
||||
BUILD_DEPENDS+= lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
|
||||
|
||||
@ -1,3 +1,2 @@
|
||||
MD5 (coq-8.2pl1.tar.gz) = 36eed48bc63ada8abf27f96eb126906c
|
||||
SHA256 (coq-8.2pl1.tar.gz) = 7c15acfd369111e51d937cce632d22fc77a6718a5ac9f2dd2dcbdfab4256ae0c
|
||||
SIZE (coq-8.2pl1.tar.gz) = 3600620
|
||||
SHA256 (coq-8.3.tar.gz) = bd818e053948e6eed288753fe10fe2b23bdc6f277a8fe50a6233d8f07b263e0a
|
||||
SIZE (coq-8.3.tar.gz) = 3736420
|
||||
|
||||
47
math/coq/files/ide-coqide.diff
Normal file
47
math/coq/files/ide-coqide.diff
Normal file
@ -0,0 +1,47 @@
|
||||
--- coq-8.3/ide/coqide.ml 2010-07-24 17:57:30.000000000 +0200
|
||||
+++ coq-8.3/ide/coqide.ml 2010-11-04 23:09:29.000000000 +0100
|
||||
@@ -251,27 +251,29 @@
|
||||
end
|
||||
|
||||
let do_if_not_computing text f x =
|
||||
- if Mutex.try_lock coq_computing then
|
||||
- let threaded_task () =
|
||||
- prerr_endline "Getting lock";
|
||||
- try
|
||||
- f x;
|
||||
- prerr_endline "Releasing lock";
|
||||
- Mutex.unlock coq_computing;
|
||||
- with e ->
|
||||
- prerr_endline "Releasing lock (on error)";
|
||||
- Mutex.unlock coq_computing;
|
||||
- raise e
|
||||
- in
|
||||
+ let threaded_task () =
|
||||
+ if Mutex.try_lock coq_computing then
|
||||
+ begin
|
||||
+ prerr_endline "Getting lock";
|
||||
+ try
|
||||
+ f x;
|
||||
+ prerr_endline "Releasing lock";
|
||||
+ Mutex.unlock coq_computing;
|
||||
+ with e ->
|
||||
+ prerr_endline "Releasing lock (on error)";
|
||||
+ Mutex.unlock coq_computing;
|
||||
+ raise e
|
||||
+ end
|
||||
+ else
|
||||
+ prerr_endline
|
||||
+ "Discarded order (computations are ongoing)"
|
||||
+ in
|
||||
prerr_endline ("Launching thread " ^ text);
|
||||
ignore (Glib.Timeout.add ~ms:300 ~callback:
|
||||
(fun () -> if Mutex.try_lock coq_computing
|
||||
then (Mutex.unlock coq_computing; false)
|
||||
else (pbar#pulse (); true)));
|
||||
ignore (Thread.create threaded_task ())
|
||||
- else
|
||||
- prerr_endline
|
||||
- "Discarded order (computations are ongoing)"
|
||||
|
||||
(* XXX - 1 appel *)
|
||||
let kill_input_view i =
|
||||
@ -1,5 +1,3 @@
|
||||
bin/coq-interface
|
||||
bin/coq-interface.opt
|
||||
bin/coq-tex
|
||||
bin/coq_makefile
|
||||
bin/coqc
|
||||
@ -16,162 +14,40 @@ bin/coqtop.byte
|
||||
bin/coqtop.opt
|
||||
bin/coqwc
|
||||
bin/gallina
|
||||
bin/coq-parser
|
||||
bin/coq-parser.opt
|
||||
lib/coq/config/coq_config.cmi
|
||||
lib/coq/config/coq_config.cmo
|
||||
lib/coq/config/coq_config.cmx
|
||||
lib/coq/config/coq_config.o
|
||||
lib/coq/contrib/cc/ccalgo.cmi
|
||||
lib/coq/contrib/cc/ccproof.cmi
|
||||
lib/coq/contrib/cc/cctac.cmi
|
||||
lib/coq/contrib/cc/g_congruence.cmi
|
||||
lib/coq/contrib/contrib.a
|
||||
lib/coq/contrib/contrib.cma
|
||||
lib/coq/contrib/contrib.cmxa
|
||||
lib/coq/contrib/dp/Dp.vo
|
||||
lib/coq/contrib/dp/dp.cmi
|
||||
lib/coq/contrib/dp/dp_gappa.cmi
|
||||
lib/coq/contrib/dp/dp_why.cmi
|
||||
lib/coq/contrib/dp/dp_zenon.cmi
|
||||
lib/coq/contrib/dp/g_dp.cmi
|
||||
lib/coq/contrib/extraction/common.cmi
|
||||
lib/coq/contrib/extraction/extract_env.cmi
|
||||
lib/coq/contrib/extraction/extraction.cmi
|
||||
lib/coq/contrib/extraction/g_extraction.cmi
|
||||
lib/coq/contrib/extraction/haskell.cmi
|
||||
lib/coq/contrib/extraction/mlutil.cmi
|
||||
lib/coq/contrib/extraction/modutil.cmi
|
||||
lib/coq/contrib/extraction/ocaml.cmi
|
||||
lib/coq/contrib/extraction/scheme.cmi
|
||||
lib/coq/contrib/extraction/table.cmi
|
||||
lib/coq/contrib/field/LegacyField.vo
|
||||
lib/coq/contrib/field/LegacyField_Compl.vo
|
||||
lib/coq/contrib/field/LegacyField_Tactic.vo
|
||||
lib/coq/contrib/field/LegacyField_Theory.vo
|
||||
lib/coq/contrib/field/field.cmi
|
||||
lib/coq/contrib/firstorder/formula.cmi
|
||||
lib/coq/contrib/firstorder/g_ground.cmi
|
||||
lib/coq/contrib/firstorder/ground.cmi
|
||||
lib/coq/contrib/firstorder/instances.cmi
|
||||
lib/coq/contrib/firstorder/rules.cmi
|
||||
lib/coq/contrib/firstorder/sequent.cmi
|
||||
lib/coq/contrib/firstorder/unify.cmi
|
||||
lib/coq/contrib/fourier/Fourier.vo
|
||||
lib/coq/contrib/fourier/Fourier_util.vo
|
||||
lib/coq/contrib/fourier/fourier.cmi
|
||||
lib/coq/contrib/fourier/fourierR.cmi
|
||||
lib/coq/contrib/fourier/g_fourier.cmi
|
||||
lib/coq/contrib/funind/Recdef.vo
|
||||
lib/coq/contrib/funind/functional_principles_proofs.cmi
|
||||
lib/coq/contrib/funind/functional_principles_types.cmi
|
||||
lib/coq/contrib/funind/g_indfun.cmi
|
||||
lib/coq/contrib/funind/indfun.cmi
|
||||
lib/coq/contrib/funind/indfun_common.cmi
|
||||
lib/coq/contrib/funind/invfun.cmi
|
||||
lib/coq/contrib/funind/merge.cmi
|
||||
lib/coq/contrib/funind/rawterm_to_relation.cmi
|
||||
lib/coq/contrib/funind/rawtermops.cmi
|
||||
lib/coq/contrib/funind/recdef.cmi
|
||||
lib/coq/contrib/interface/vernacrc
|
||||
lib/coq/contrib/micromega/CheckerMaker.vo
|
||||
lib/coq/contrib/micromega/Env.vo
|
||||
lib/coq/contrib/micromega/EnvRing.vo
|
||||
lib/coq/contrib/micromega/OrderedRing.vo
|
||||
lib/coq/contrib/micromega/Psatz.vo
|
||||
lib/coq/contrib/micromega/QMicromega.vo
|
||||
lib/coq/contrib/micromega/RMicromega.vo
|
||||
lib/coq/contrib/micromega/Refl.vo
|
||||
lib/coq/contrib/micromega/RingMicromega.vo
|
||||
lib/coq/contrib/micromega/Tauto.vo
|
||||
lib/coq/contrib/micromega/VarMap.vo
|
||||
lib/coq/contrib/micromega/ZCoeff.vo
|
||||
lib/coq/contrib/micromega/ZMicromega.vo
|
||||
lib/coq/contrib/micromega/certificate.cmi
|
||||
lib/coq/contrib/micromega/coq_micromega.cmi
|
||||
lib/coq/contrib/micromega/csdpcert
|
||||
lib/coq/contrib/micromega/g_micromega.cmi
|
||||
lib/coq/contrib/micromega/mfourier.cmi
|
||||
lib/coq/contrib/micromega/micromega.cmi
|
||||
lib/coq/contrib/micromega/mutils.cmi
|
||||
lib/coq/contrib/micromega/vector.cmi
|
||||
lib/coq/contrib/omega/Omega.vo
|
||||
lib/coq/contrib/omega/OmegaLemmas.vo
|
||||
lib/coq/contrib/omega/PreOmega.vo
|
||||
lib/coq/contrib/omega/coq_omega.cmi
|
||||
lib/coq/contrib/omega/g_omega.cmi
|
||||
lib/coq/contrib/omega/omega.cmi
|
||||
lib/coq/contrib/ring/LegacyArithRing.vo
|
||||
lib/coq/contrib/ring/LegacyNArithRing.vo
|
||||
lib/coq/contrib/ring/LegacyRing.vo
|
||||
lib/coq/contrib/ring/LegacyRing_theory.vo
|
||||
lib/coq/contrib/ring/LegacyZArithRing.vo
|
||||
lib/coq/contrib/ring/Quote.vo
|
||||
lib/coq/contrib/ring/Ring_abstract.vo
|
||||
lib/coq/contrib/ring/Ring_normalize.vo
|
||||
lib/coq/contrib/ring/Setoid_ring.vo
|
||||
lib/coq/contrib/ring/Setoid_ring_normalize.vo
|
||||
lib/coq/contrib/ring/Setoid_ring_theory.vo
|
||||
lib/coq/contrib/ring/g_quote.cmi
|
||||
lib/coq/contrib/ring/g_ring.cmi
|
||||
lib/coq/contrib/ring/quote.cmi
|
||||
lib/coq/contrib/ring/ring.cmi
|
||||
lib/coq/contrib/romega/ROmega.vo
|
||||
lib/coq/contrib/romega/ReflOmegaCore.vo
|
||||
lib/coq/contrib/romega/const_omega.cmi
|
||||
lib/coq/contrib/romega/g_romega.cmi
|
||||
lib/coq/contrib/romega/refl_omega.cmi
|
||||
lib/coq/contrib/rtauto/Bintree.vo
|
||||
lib/coq/contrib/rtauto/Rtauto.vo
|
||||
lib/coq/contrib/rtauto/g_rtauto.cmi
|
||||
lib/coq/contrib/rtauto/proof_search.cmi
|
||||
lib/coq/contrib/rtauto/refl_tauto.cmi
|
||||
lib/coq/contrib/setoid_ring/ArithRing.vo
|
||||
lib/coq/contrib/setoid_ring/BinList.vo
|
||||
lib/coq/contrib/setoid_ring/Field.vo
|
||||
lib/coq/contrib/setoid_ring/Field_tac.vo
|
||||
lib/coq/contrib/setoid_ring/Field_theory.vo
|
||||
lib/coq/contrib/setoid_ring/InitialRing.vo
|
||||
lib/coq/contrib/setoid_ring/NArithRing.vo
|
||||
lib/coq/contrib/setoid_ring/RealField.vo
|
||||
lib/coq/contrib/setoid_ring/Ring.vo
|
||||
lib/coq/contrib/setoid_ring/Ring_base.vo
|
||||
lib/coq/contrib/setoid_ring/Ring_equiv.vo
|
||||
lib/coq/contrib/setoid_ring/Ring_polynom.vo
|
||||
lib/coq/contrib/setoid_ring/Ring_tac.vo
|
||||
lib/coq/contrib/setoid_ring/Ring_theory.vo
|
||||
lib/coq/contrib/setoid_ring/ZArithRing.vo
|
||||
lib/coq/contrib/setoid_ring/newring.cmi
|
||||
lib/coq/contrib/subtac/equations.cmi
|
||||
lib/coq/contrib/subtac/eterm.cmi
|
||||
lib/coq/contrib/subtac/g_eterm.cmi
|
||||
lib/coq/contrib/subtac/g_subtac.cmi
|
||||
lib/coq/contrib/subtac/subtac.cmi
|
||||
lib/coq/contrib/subtac/subtac_cases.cmi
|
||||
lib/coq/contrib/subtac/subtac_classes.cmi
|
||||
lib/coq/contrib/subtac/subtac_coercion.cmi
|
||||
lib/coq/contrib/subtac/subtac_command.cmi
|
||||
lib/coq/contrib/subtac/subtac_errors.cmi
|
||||
lib/coq/contrib/subtac/subtac_obligations.cmi
|
||||
lib/coq/contrib/subtac/subtac_pretyping.cmi
|
||||
lib/coq/contrib/subtac/subtac_pretyping_F.cmi
|
||||
lib/coq/contrib/subtac/subtac_utils.cmi
|
||||
lib/coq/contrib/xml/acic.cmi
|
||||
lib/coq/contrib/xml/acic2Xml.cmi
|
||||
lib/coq/contrib/xml/cic2Xml.cmi
|
||||
lib/coq/contrib/xml/cic2acic.cmi
|
||||
lib/coq/contrib/xml/doubleTypeInference.cmi
|
||||
lib/coq/contrib/xml/dumptree.cmi
|
||||
lib/coq/contrib/xml/proof2aproof.cmi
|
||||
lib/coq/contrib/xml/proofTree2Xml.cmi
|
||||
lib/coq/contrib/xml/unshare.cmi
|
||||
lib/coq/contrib/xml/xml.cmi
|
||||
lib/coq/contrib/xml/xmlcommand.cmi
|
||||
lib/coq/contrib/xml/xmlentries.cmi
|
||||
lib/coq/dllcoqrun.so
|
||||
%%IDE%%lib/coq/ide/.coqide-gtk2rc
|
||||
%%IDE%%lib/coq/ide/FAQ
|
||||
%%IDE%%lib/coq/ide/command_windows.cmi
|
||||
%%IDE%%lib/coq/ide/config_lexer.cmi
|
||||
%%IDE%%lib/coq/ide/config_parser.cmi
|
||||
%%IDE%%lib/coq/ide/coq.cmi
|
||||
%%IDE%%lib/coq/ide/coq.png
|
||||
%%IDE%%lib/coq/ide/coq_commands.cmi
|
||||
%%IDE%%lib/coq/ide/coq_lex.cmi
|
||||
%%IDE%%lib/coq/ide/coq_tactics.cmi
|
||||
%%IDE%%lib/coq/ide/coqide.cmi
|
||||
%%IDE%%lib/coq/ide/gtk_parsing.cmi
|
||||
%%IDE%%lib/coq/ide/ide.a
|
||||
%%IDE%%lib/coq/ide/ide.cma
|
||||
%%IDE%%lib/coq/ide/ide.cmxa
|
||||
%%IDE%%lib/coq/ide/ideutils.cmi
|
||||
%%IDE%%lib/coq/ide/preferences.cmi
|
||||
%%IDE%%lib/coq/ide/tags.cmi
|
||||
%%IDE%%lib/coq/ide/typed_notebook.cmi
|
||||
%%IDE%%lib/coq/ide/undo.cmi
|
||||
%%IDE%%lib/coq/ide/utf8_convert.cmi
|
||||
%%IDE%%lib/coq/ide/utils/config_file.cmi
|
||||
%%IDE%%lib/coq/ide/utils/configwin.cmi
|
||||
%%IDE%%lib/coq/ide/utils/configwin_ihm.cmi
|
||||
%%IDE%%lib/coq/ide/utils/configwin_keys.cmi
|
||||
%%IDE%%lib/coq/ide/utils/configwin_messages.cmi
|
||||
%%IDE%%lib/coq/ide/utils/configwin_types.cmi
|
||||
%%IDE%%lib/coq/ide/utils/editable_cells.cmi
|
||||
%%IDE%%lib/coq/ide/utils/okey.cmi
|
||||
lib/coq/interp/constrextern.cmi
|
||||
lib/coq/interp/constrintern.cmi
|
||||
lib/coq/interp/coqlib.cmi
|
||||
@ -185,6 +61,7 @@ lib/coq/interp/modintern.cmi
|
||||
lib/coq/interp/notation.cmi
|
||||
lib/coq/interp/ppextend.cmi
|
||||
lib/coq/interp/reserve.cmi
|
||||
lib/coq/interp/smartlocate.cmi
|
||||
lib/coq/interp/syntax_def.cmi
|
||||
lib/coq/interp/topconstr.cmi
|
||||
lib/coq/kernel/cbytecodes.cmi
|
||||
@ -224,11 +101,14 @@ lib/coq/kernel/vm.cmi
|
||||
lib/coq/lib/bigint.cmi
|
||||
lib/coq/lib/bstack.cmi
|
||||
lib/coq/lib/compat.cmi
|
||||
lib/coq/lib/dnet.cmi
|
||||
lib/coq/lib/dyn.cmi
|
||||
lib/coq/lib/edit.cmi
|
||||
lib/coq/lib/envars.cmi
|
||||
lib/coq/lib/explore.cmi
|
||||
lib/coq/lib/flags.cmi
|
||||
lib/coq/lib/fmap.cmi
|
||||
lib/coq/lib/fset.cmi
|
||||
lib/coq/lib/gmap.cmi
|
||||
lib/coq/lib/gmapl.cmi
|
||||
lib/coq/lib/gset.cmi
|
||||
@ -243,8 +123,11 @@ lib/coq/lib/pp_control.cmi
|
||||
lib/coq/lib/predicate.cmi
|
||||
lib/coq/lib/profile.cmi
|
||||
lib/coq/lib/rtree.cmi
|
||||
lib/coq/lib/segmenttree.cmi
|
||||
lib/coq/lib/system.cmi
|
||||
lib/coq/lib/tlm.cmi
|
||||
lib/coq/lib/tries.cmi
|
||||
lib/coq/lib/unicodetable.cmi
|
||||
lib/coq/lib/util.cmi
|
||||
lib/coq/libcoqrun.a
|
||||
lib/coq/library/decl_kinds.cmi
|
||||
@ -269,20 +152,15 @@ lib/coq/library/states.cmi
|
||||
lib/coq/library/summary.cmi
|
||||
lib/coq/parsing/egrammar.cmi
|
||||
lib/coq/parsing/extend.cmi
|
||||
lib/coq/parsing/g_ascii_syntax.cmi
|
||||
lib/coq/parsing/extrawit.cmi
|
||||
lib/coq/parsing/g_constr.cmi
|
||||
lib/coq/parsing/g_decl_mode.cmi
|
||||
lib/coq/parsing/g_intsyntax.cmi
|
||||
lib/coq/parsing/g_ltac.cmi
|
||||
lib/coq/parsing/g_natsyntax.cmi
|
||||
lib/coq/parsing/g_prim.cmi
|
||||
lib/coq/parsing/g_proofs.cmi
|
||||
lib/coq/parsing/g_rsyntax.cmi
|
||||
lib/coq/parsing/g_string_syntax.cmi
|
||||
lib/coq/parsing/g_tactic.cmi
|
||||
lib/coq/parsing/g_vernac.cmi
|
||||
lib/coq/parsing/g_xml.cmi
|
||||
lib/coq/parsing/g_zsyntax.cmi
|
||||
lib/coq/parsing/grammar.cma
|
||||
lib/coq/parsing/highparsing.a
|
||||
lib/coq/parsing/highparsing.cma
|
||||
@ -299,8 +177,236 @@ lib/coq/parsing/ppvernac.cmi
|
||||
lib/coq/parsing/prettyp.cmi
|
||||
lib/coq/parsing/printer.cmi
|
||||
lib/coq/parsing/printmod.cmi
|
||||
lib/coq/parsing/search.cmi
|
||||
lib/coq/parsing/tactic_printer.cmi
|
||||
lib/coq/plugins/cc/cc_plugin.cma
|
||||
lib/coq/plugins/cc/cc_plugin.cmxs
|
||||
lib/coq/plugins/cc/cc_plugin_mod.cmi
|
||||
lib/coq/plugins/cc/ccalgo.cmi
|
||||
lib/coq/plugins/cc/ccproof.cmi
|
||||
lib/coq/plugins/cc/cctac.cmi
|
||||
lib/coq/plugins/cc/g_congruence.cmi
|
||||
lib/coq/plugins/dp/Dp.vo
|
||||
lib/coq/plugins/dp/dp.cmi
|
||||
lib/coq/plugins/dp/dp_plugin.cma
|
||||
lib/coq/plugins/dp/dp_plugin.cmxs
|
||||
lib/coq/plugins/dp/dp_plugin_mod.cmi
|
||||
lib/coq/plugins/dp/dp_why.cmi
|
||||
lib/coq/plugins/dp/dp_zenon.cmi
|
||||
lib/coq/plugins/dp/g_dp.cmi
|
||||
lib/coq/plugins/extraction/ExtrOcamlBasic.vo
|
||||
lib/coq/plugins/extraction/ExtrOcamlBigIntConv.vo
|
||||
lib/coq/plugins/extraction/ExtrOcamlIntConv.vo
|
||||
lib/coq/plugins/extraction/ExtrOcamlNatBigInt.vo
|
||||
lib/coq/plugins/extraction/ExtrOcamlNatInt.vo
|
||||
lib/coq/plugins/extraction/ExtrOcamlString.vo
|
||||
lib/coq/plugins/extraction/ExtrOcamlZBigInt.vo
|
||||
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.cmxs
|
||||
lib/coq/plugins/extraction/extraction_plugin_mod.cmi
|
||||
lib/coq/plugins/extraction/g_extraction.cmi
|
||||
lib/coq/plugins/extraction/haskell.cmi
|
||||
lib/coq/plugins/extraction/mlutil.cmi
|
||||
lib/coq/plugins/extraction/modutil.cmi
|
||||
lib/coq/plugins/extraction/ocaml.cmi
|
||||
lib/coq/plugins/extraction/scheme.cmi
|
||||
lib/coq/plugins/extraction/table.cmi
|
||||
lib/coq/plugins/field/LegacyField.vo
|
||||
lib/coq/plugins/field/LegacyField_Compl.vo
|
||||
lib/coq/plugins/field/LegacyField_Tactic.vo
|
||||
lib/coq/plugins/field/LegacyField_Theory.vo
|
||||
lib/coq/plugins/field/field.cmi
|
||||
lib/coq/plugins/field/field_plugin.cma
|
||||
lib/coq/plugins/field/field_plugin.cmxs
|
||||
lib/coq/plugins/field/field_plugin_mod.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.cmxs
|
||||
lib/coq/plugins/firstorder/ground_plugin_mod.cmi
|
||||
lib/coq/plugins/firstorder/instances.cmi
|
||||
lib/coq/plugins/firstorder/rules.cmi
|
||||
lib/coq/plugins/firstorder/sequent.cmi
|
||||
lib/coq/plugins/firstorder/unify.cmi
|
||||
lib/coq/plugins/fourier/Fourier.vo
|
||||
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.cmxs
|
||||
lib/coq/plugins/fourier/fourier_plugin_mod.cmi
|
||||
lib/coq/plugins/fourier/g_fourier.cmi
|
||||
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/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/rawterm_to_relation.cmi
|
||||
lib/coq/plugins/funind/rawtermops.cmi
|
||||
lib/coq/plugins/funind/recdef.cmi
|
||||
lib/coq/plugins/funind/recdef_plugin.cma
|
||||
lib/coq/plugins/funind/recdef_plugin.cmxs
|
||||
lib/coq/plugins/funind/recdef_plugin_mod.cmi
|
||||
lib/coq/plugins/micromega/CheckerMaker.vo
|
||||
lib/coq/plugins/micromega/Env.vo
|
||||
lib/coq/plugins/micromega/EnvRing.vo
|
||||
lib/coq/plugins/micromega/OrderedRing.vo
|
||||
lib/coq/plugins/micromega/Psatz.vo
|
||||
lib/coq/plugins/micromega/QMicromega.vo
|
||||
lib/coq/plugins/micromega/RMicromega.vo
|
||||
lib/coq/plugins/micromega/Refl.vo
|
||||
lib/coq/plugins/micromega/RingMicromega.vo
|
||||
lib/coq/plugins/micromega/Tauto.vo
|
||||
lib/coq/plugins/micromega/VarMap.vo
|
||||
lib/coq/plugins/micromega/ZCoeff.vo
|
||||
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.cmxs
|
||||
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/sos_types.cmi
|
||||
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.cmxs
|
||||
lib/coq/plugins/nsatz/nsatz_plugin_mod.cmi
|
||||
lib/coq/plugins/nsatz/polynom.cmi
|
||||
lib/coq/plugins/nsatz/utile.cmi
|
||||
lib/coq/plugins/omega/Omega.vo
|
||||
lib/coq/plugins/omega/OmegaLemmas.vo
|
||||
lib/coq/plugins/omega/OmegaPlugin.vo
|
||||
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.cmxs
|
||||
lib/coq/plugins/omega/omega_plugin_mod.cmi
|
||||
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.cmxs
|
||||
lib/coq/plugins/quote/quote_plugin_mod.cmi
|
||||
lib/coq/plugins/ring/LegacyArithRing.vo
|
||||
lib/coq/plugins/ring/LegacyNArithRing.vo
|
||||
lib/coq/plugins/ring/LegacyRing.vo
|
||||
lib/coq/plugins/ring/LegacyRing_theory.vo
|
||||
lib/coq/plugins/ring/LegacyZArithRing.vo
|
||||
lib/coq/plugins/ring/Ring_abstract.vo
|
||||
lib/coq/plugins/ring/Ring_normalize.vo
|
||||
lib/coq/plugins/ring/Setoid_ring.vo
|
||||
lib/coq/plugins/ring/Setoid_ring_normalize.vo
|
||||
lib/coq/plugins/ring/Setoid_ring_theory.vo
|
||||
lib/coq/plugins/ring/g_ring.cmi
|
||||
lib/coq/plugins/ring/ring.cmi
|
||||
lib/coq/plugins/ring/ring_plugin.cma
|
||||
lib/coq/plugins/ring/ring_plugin.cmxs
|
||||
lib/coq/plugins/ring/ring_plugin_mod.cmi
|
||||
lib/coq/plugins/romega/ROmega.vo
|
||||
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.cmxs
|
||||
lib/coq/plugins/romega/romega_plugin_mod.cmi
|
||||
lib/coq/plugins/rtauto/Bintree.vo
|
||||
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.cmxs
|
||||
lib/coq/plugins/rtauto/rtauto_plugin_mod.cmi
|
||||
lib/coq/plugins/setoid_ring/ArithRing.vo
|
||||
lib/coq/plugins/setoid_ring/BinList.vo
|
||||
lib/coq/plugins/setoid_ring/Field.vo
|
||||
lib/coq/plugins/setoid_ring/Field_tac.vo
|
||||
lib/coq/plugins/setoid_ring/Field_theory.vo
|
||||
lib/coq/plugins/setoid_ring/InitialRing.vo
|
||||
lib/coq/plugins/setoid_ring/NArithRing.vo
|
||||
lib/coq/plugins/setoid_ring/RealField.vo
|
||||
lib/coq/plugins/setoid_ring/Ring.vo
|
||||
lib/coq/plugins/setoid_ring/Ring_base.vo
|
||||
lib/coq/plugins/setoid_ring/Ring_equiv.vo
|
||||
lib/coq/plugins/setoid_ring/Ring_polynom.vo
|
||||
lib/coq/plugins/setoid_ring/Ring_tac.vo
|
||||
lib/coq/plugins/setoid_ring/Ring_theory.vo
|
||||
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.cmxs
|
||||
lib/coq/plugins/setoid_ring/newring_plugin_mod.cmi
|
||||
lib/coq/plugins/subtac/eterm.cmi
|
||||
lib/coq/plugins/subtac/g_subtac.cmi
|
||||
lib/coq/plugins/subtac/subtac.cmi
|
||||
lib/coq/plugins/subtac/subtac_cases.cmi
|
||||
lib/coq/plugins/subtac/subtac_classes.cmi
|
||||
lib/coq/plugins/subtac/subtac_coercion.cmi
|
||||
lib/coq/plugins/subtac/subtac_command.cmi
|
||||
lib/coq/plugins/subtac/subtac_errors.cmi
|
||||
lib/coq/plugins/subtac/subtac_obligations.cmi
|
||||
lib/coq/plugins/subtac/subtac_plugin.cma
|
||||
lib/coq/plugins/subtac/subtac_plugin.cmxs
|
||||
lib/coq/plugins/subtac/subtac_plugin_mod.cmi
|
||||
lib/coq/plugins/subtac/subtac_pretyping.cmi
|
||||
lib/coq/plugins/subtac/subtac_pretyping_F.cmi
|
||||
lib/coq/plugins/subtac/subtac_utils.cmi
|
||||
lib/coq/plugins/syntax/ascii_syntax.cmi
|
||||
lib/coq/plugins/syntax/ascii_syntax_plugin.cma
|
||||
lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
|
||||
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.cmxs
|
||||
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.cmxs
|
||||
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.cmxs
|
||||
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.cmxs
|
||||
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.cmxs
|
||||
lib/coq/plugins/syntax/z_syntax_plugin_mod.cmi
|
||||
lib/coq/plugins/xml/acic.cmi
|
||||
lib/coq/plugins/xml/acic2Xml.cmi
|
||||
lib/coq/plugins/xml/cic2Xml.cmi
|
||||
lib/coq/plugins/xml/cic2acic.cmi
|
||||
lib/coq/plugins/xml/doubleTypeInference.cmi
|
||||
lib/coq/plugins/xml/dumptree.cmi
|
||||
lib/coq/plugins/xml/proof2aproof.cmi
|
||||
lib/coq/plugins/xml/proofTree2Xml.cmi
|
||||
lib/coq/plugins/xml/unshare.cmi
|
||||
lib/coq/plugins/xml/xml.cmi
|
||||
lib/coq/plugins/xml/xml_plugin.cma
|
||||
lib/coq/plugins/xml/xml_plugin.cmxs
|
||||
lib/coq/plugins/xml/xml_plugin_mod.cmi
|
||||
lib/coq/plugins/xml/xmlcommand.cmi
|
||||
lib/coq/plugins/xml/xmlentries.cmi
|
||||
lib/coq/pretyping/cases.cmi
|
||||
lib/coq/pretyping/cbv.cmi
|
||||
lib/coq/pretyping/classops.cmi
|
||||
@ -313,6 +419,7 @@ lib/coq/pretyping/evd.cmi
|
||||
lib/coq/pretyping/indrec.cmi
|
||||
lib/coq/pretyping/inductiveops.cmi
|
||||
lib/coq/pretyping/matching.cmi
|
||||
lib/coq/pretyping/namegen.cmi
|
||||
lib/coq/pretyping/pattern.cmi
|
||||
lib/coq/pretyping/pretype_errors.cmi
|
||||
lib/coq/pretyping/pretyping.a
|
||||
@ -324,6 +431,7 @@ lib/coq/pretyping/recordops.cmi
|
||||
lib/coq/pretyping/reductionops.cmi
|
||||
lib/coq/pretyping/retyping.cmi
|
||||
lib/coq/pretyping/tacred.cmi
|
||||
lib/coq/pretyping/term_dnet.cmi
|
||||
lib/coq/pretyping/termops.cmi
|
||||
lib/coq/pretyping/typeclasses.cmi
|
||||
lib/coq/pretyping/typeclasses_errors.cmi
|
||||
@ -357,7 +465,9 @@ lib/coq/tactics/dhyp.cmi
|
||||
lib/coq/tactics/dn.cmi
|
||||
lib/coq/tactics/eauto.cmi
|
||||
lib/coq/tactics/elim.cmi
|
||||
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
|
||||
@ -371,7 +481,9 @@ lib/coq/tactics/inv.cmi
|
||||
lib/coq/tactics/leminv.cmi
|
||||
lib/coq/tactics/nbtermdn.cmi
|
||||
lib/coq/tactics/refine.cmi
|
||||
lib/coq/tactics/rewrite.cmi
|
||||
lib/coq/tactics/tacinterp.cmi
|
||||
lib/coq/tactics/tactic_option.cmi
|
||||
lib/coq/tactics/tacticals.cmi
|
||||
lib/coq/tactics/tactics.a
|
||||
lib/coq/tactics/tactics.cma
|
||||
@ -395,8 +507,10 @@ lib/coq/theories/Arith/Le.vo
|
||||
lib/coq/theories/Arith/Lt.vo
|
||||
lib/coq/theories/Arith/Max.vo
|
||||
lib/coq/theories/Arith/Min.vo
|
||||
lib/coq/theories/Arith/MinMax.vo
|
||||
lib/coq/theories/Arith/Minus.vo
|
||||
lib/coq/theories/Arith/Mult.vo
|
||||
lib/coq/theories/Arith/NatOrderedType.vo
|
||||
lib/coq/theories/Arith/Peano_dec.vo
|
||||
lib/coq/theories/Arith/Plus.vo
|
||||
lib/coq/theories/Arith/Wf_nat.vo
|
||||
@ -409,13 +523,12 @@ lib/coq/theories/Bool/Sumbool.vo
|
||||
lib/coq/theories/Bool/Zerob.vo
|
||||
lib/coq/theories/Classes/EquivDec.vo
|
||||
lib/coq/theories/Classes/Equivalence.vo
|
||||
lib/coq/theories/Classes/Functions.vo
|
||||
lib/coq/theories/Classes/Init.vo
|
||||
lib/coq/theories/Classes/Morphisms.vo
|
||||
lib/coq/theories/Classes/Morphisms_Prop.vo
|
||||
lib/coq/theories/Classes/Morphisms_Relations.vo
|
||||
lib/coq/theories/Classes/RelationClasses.vo
|
||||
lib/coq/theories/Classes/SetoidAxioms.vo
|
||||
lib/coq/theories/Classes/RelationPairs.vo
|
||||
lib/coq/theories/Classes/SetoidClass.vo
|
||||
lib/coq/theories/Classes/SetoidDec.vo
|
||||
lib/coq/theories/Classes/SetoidTactics.vo
|
||||
@ -429,19 +542,17 @@ lib/coq/theories/FSets/FMapWeakList.vo
|
||||
lib/coq/theories/FSets/FMaps.vo
|
||||
lib/coq/theories/FSets/FSetAVL.vo
|
||||
lib/coq/theories/FSets/FSetBridge.vo
|
||||
lib/coq/theories/FSets/FSetCompat.vo
|
||||
lib/coq/theories/FSets/FSetDecide.vo
|
||||
lib/coq/theories/FSets/FSetEqProperties.vo
|
||||
lib/coq/theories/FSets/FSetFacts.vo
|
||||
lib/coq/theories/FSets/FSetFullAVL.vo
|
||||
lib/coq/theories/FSets/FSetInterface.vo
|
||||
lib/coq/theories/FSets/FSetList.vo
|
||||
lib/coq/theories/FSets/FSetPositive.vo
|
||||
lib/coq/theories/FSets/FSetProperties.vo
|
||||
lib/coq/theories/FSets/FSetToFiniteSet.vo
|
||||
lib/coq/theories/FSets/FSetWeakList.vo
|
||||
lib/coq/theories/FSets/FSets.vo
|
||||
lib/coq/theories/FSets/OrderedType.vo
|
||||
lib/coq/theories/FSets/OrderedTypeAlt.vo
|
||||
lib/coq/theories/FSets/OrderedTypeEx.vo
|
||||
lib/coq/theories/Init/Datatypes.vo
|
||||
lib/coq/theories/Init/Logic.vo
|
||||
lib/coq/theories/Init/Logic_Type.vo
|
||||
@ -454,7 +565,6 @@ lib/coq/theories/Init/Wf.vo
|
||||
lib/coq/theories/Lists/List.vo
|
||||
lib/coq/theories/Lists/ListSet.vo
|
||||
lib/coq/theories/Lists/ListTactics.vo
|
||||
lib/coq/theories/Lists/MonoList.vo
|
||||
lib/coq/theories/Lists/SetoidList.vo
|
||||
lib/coq/theories/Lists/StreamMemo.vo
|
||||
lib/coq/theories/Lists/Streams.vo
|
||||
@ -473,8 +583,6 @@ lib/coq/theories/Logic/Classical_Prop.vo
|
||||
lib/coq/theories/Logic/Classical_Type.vo
|
||||
lib/coq/theories/Logic/ConstructiveEpsilon.vo
|
||||
lib/coq/theories/Logic/Decidable.vo
|
||||
lib/coq/theories/Logic/DecidableType.vo
|
||||
lib/coq/theories/Logic/DecidableTypeEx.vo
|
||||
lib/coq/theories/Logic/Description.vo
|
||||
lib/coq/theories/Logic/Diaconescu.vo
|
||||
lib/coq/theories/Logic/Epsilon.vo
|
||||
@ -489,13 +597,28 @@ lib/coq/theories/Logic/ProofIrrelevance.vo
|
||||
lib/coq/theories/Logic/ProofIrrelevanceFacts.vo
|
||||
lib/coq/theories/Logic/RelationalChoice.vo
|
||||
lib/coq/theories/Logic/SetIsType.vo
|
||||
lib/coq/theories/MSets/MSetAVL.vo
|
||||
lib/coq/theories/MSets/MSetDecide.vo
|
||||
lib/coq/theories/MSets/MSetEqProperties.vo
|
||||
lib/coq/theories/MSets/MSetFacts.vo
|
||||
lib/coq/theories/MSets/MSetInterface.vo
|
||||
lib/coq/theories/MSets/MSetList.vo
|
||||
lib/coq/theories/MSets/MSetPositive.vo
|
||||
lib/coq/theories/MSets/MSetProperties.vo
|
||||
lib/coq/theories/MSets/MSetToFiniteSet.vo
|
||||
lib/coq/theories/MSets/MSetWeakList.vo
|
||||
lib/coq/theories/MSets/MSets.vo
|
||||
lib/coq/theories/NArith/BinNat.vo
|
||||
lib/coq/theories/NArith/BinPos.vo
|
||||
lib/coq/theories/NArith/NArith.vo
|
||||
lib/coq/theories/NArith/NOrderedType.vo
|
||||
lib/coq/theories/NArith/Ndec.vo
|
||||
lib/coq/theories/NArith/Ndigits.vo
|
||||
lib/coq/theories/NArith/Ndist.vo
|
||||
lib/coq/theories/NArith/Nminmax.vo
|
||||
lib/coq/theories/NArith/Nnat.vo
|
||||
lib/coq/theories/NArith/POrderedType.vo
|
||||
lib/coq/theories/NArith/Pminmax.vo
|
||||
lib/coq/theories/NArith/Pnat.vo
|
||||
lib/coq/theories/Numbers/BigNumPrelude.vo
|
||||
lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
|
||||
@ -512,14 +635,20 @@ lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo
|
||||
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo
|
||||
lib/coq/theories/Numbers/Cyclic/Int31/Cyclic31.vo
|
||||
lib/coq/theories/Numbers/Cyclic/Int31/Int31.vo
|
||||
lib/coq/theories/Numbers/Cyclic/Int31/Ring31.vo
|
||||
lib/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZAdd.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZAddOrder.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZAxioms.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZBase.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZDivEucl.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZDivFloor.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZLt.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZMul.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZProperties.vo
|
||||
lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vo
|
||||
lib/coq/theories/Numbers/Integer/BigZ/BigZ.vo
|
||||
lib/coq/theories/Numbers/Integer/BigZ/ZMake.vo
|
||||
lib/coq/theories/Numbers/Integer/Binary/ZBinary.vo
|
||||
@ -531,22 +660,28 @@ lib/coq/theories/Numbers/NatInt/NZAdd.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZAddOrder.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZAxioms.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZBase.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZDiv.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZDomain.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZMul.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZMulOrder.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZOrder.vo
|
||||
lib/coq/theories/Numbers/NatInt/NZProperties.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NAdd.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NAddOrder.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NAxioms.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NBase.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NDefOps.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NDiv.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NIso.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NMul.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NMulOrder.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NOrder.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NProperties.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NStrongRec.vo
|
||||
lib/coq/theories/Numbers/Natural/Abstract/NSub.vo
|
||||
lib/coq/theories/Numbers/Natural/BigN/BigN.vo
|
||||
lib/coq/theories/Numbers/Natural/BigN/NMake.vo
|
||||
lib/coq/theories/Numbers/Natural/BigN/NMake_gen.vo
|
||||
lib/coq/theories/Numbers/Natural/BigN/Nbasic.vo
|
||||
lib/coq/theories/Numbers/Natural/Binary/NBinDefs.vo
|
||||
lib/coq/theories/Numbers/Natural/Binary/NBinary.vo
|
||||
lib/coq/theories/Numbers/Natural/Peano/NPeano.vo
|
||||
lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.vo
|
||||
@ -566,9 +701,11 @@ lib/coq/theories/Program/Utils.vo
|
||||
lib/coq/theories/Program/Wf.vo
|
||||
lib/coq/theories/QArith/QArith.vo
|
||||
lib/coq/theories/QArith/QArith_base.vo
|
||||
lib/coq/theories/QArith/QOrderedType.vo
|
||||
lib/coq/theories/QArith/Qabs.vo
|
||||
lib/coq/theories/QArith/Qcanon.vo
|
||||
lib/coq/theories/QArith/Qfield.vo
|
||||
lib/coq/theories/QArith/Qminmax.vo
|
||||
lib/coq/theories/QArith/Qpower.vo
|
||||
lib/coq/theories/QArith/Qreals.vo
|
||||
lib/coq/theories/QArith/Qreduction.vo
|
||||
@ -591,6 +728,7 @@ lib/coq/theories/Reals/PSeries_reg.vo
|
||||
lib/coq/theories/Reals/PartSum.vo
|
||||
lib/coq/theories/Reals/RIneq.vo
|
||||
lib/coq/theories/Reals/RList.vo
|
||||
lib/coq/theories/Reals/ROrderedType.vo
|
||||
lib/coq/theories/Reals/R_Ifp.vo
|
||||
lib/coq/theories/Reals/R_sqr.vo
|
||||
lib/coq/theories/Reals/R_sqrt.vo
|
||||
@ -612,6 +750,7 @@ lib/coq/theories/Reals/RiemannInt.vo
|
||||
lib/coq/theories/Reals/RiemannInt_SF.vo
|
||||
lib/coq/theories/Reals/Rlimit.vo
|
||||
lib/coq/theories/Reals/Rlogic.vo
|
||||
lib/coq/theories/Reals/Rminmax.vo
|
||||
lib/coq/theories/Reals/Rpow_def.vo
|
||||
lib/coq/theories/Reals/Rpower.vo
|
||||
lib/coq/theories/Reals/Rprod.vo
|
||||
@ -658,13 +797,30 @@ lib/coq/theories/Sets/Relations_3.vo
|
||||
lib/coq/theories/Sets/Relations_3_facts.vo
|
||||
lib/coq/theories/Sets/Uniset.vo
|
||||
lib/coq/theories/Sorting/Heap.vo
|
||||
lib/coq/theories/Sorting/Mergesort.vo
|
||||
lib/coq/theories/Sorting/PermutEq.vo
|
||||
lib/coq/theories/Sorting/PermutSetoid.vo
|
||||
lib/coq/theories/Sorting/Permutation.vo
|
||||
lib/coq/theories/Sorting/Sorted.vo
|
||||
lib/coq/theories/Sorting/Sorting.vo
|
||||
lib/coq/theories/Strings/Ascii.vo
|
||||
lib/coq/theories/Strings/String.vo
|
||||
lib/coq/theories/Structures/DecidableType.vo
|
||||
lib/coq/theories/Structures/DecidableTypeEx.vo
|
||||
lib/coq/theories/Structures/Equalities.vo
|
||||
lib/coq/theories/Structures/EqualitiesFacts.vo
|
||||
lib/coq/theories/Structures/GenericMinMax.vo
|
||||
lib/coq/theories/Structures/OrderedType.vo
|
||||
lib/coq/theories/Structures/OrderedTypeAlt.vo
|
||||
lib/coq/theories/Structures/OrderedTypeEx.vo
|
||||
lib/coq/theories/Structures/Orders.vo
|
||||
lib/coq/theories/Structures/OrdersAlt.vo
|
||||
lib/coq/theories/Structures/OrdersEx.vo
|
||||
lib/coq/theories/Structures/OrdersFacts.vo
|
||||
lib/coq/theories/Structures/OrdersLists.vo
|
||||
lib/coq/theories/Structures/OrdersTac.vo
|
||||
lib/coq/theories/Unicode/Utf8.vo
|
||||
lib/coq/theories/Unicode/Utf8_core.vo
|
||||
lib/coq/theories/Wellfounded/Disjoint_Union.vo
|
||||
lib/coq/theories/Wellfounded/Inclusion.vo
|
||||
lib/coq/theories/Wellfounded/Inverse_Image.vo
|
||||
@ -682,11 +838,12 @@ lib/coq/theories/ZArith/ZArith_base.vo
|
||||
lib/coq/theories/ZArith/ZArith_dec.vo
|
||||
lib/coq/theories/ZArith/ZOdiv.vo
|
||||
lib/coq/theories/ZArith/ZOdiv_def.vo
|
||||
lib/coq/theories/ZArith/ZOrderedType.vo
|
||||
lib/coq/theories/ZArith/Zabs.vo
|
||||
lib/coq/theories/ZArith/Zbinary.vo
|
||||
lib/coq/theories/ZArith/Zbool.vo
|
||||
lib/coq/theories/ZArith/Zcompare.vo
|
||||
lib/coq/theories/ZArith/Zcomplements.vo
|
||||
lib/coq/theories/ZArith/Zdigits.vo
|
||||
lib/coq/theories/ZArith/Zdiv.vo
|
||||
lib/coq/theories/ZArith/Zeven.vo
|
||||
lib/coq/theories/ZArith/Zgcd_alt.vo
|
||||
@ -708,6 +865,7 @@ lib/coq/theories/ZArith/auxiliary.vo
|
||||
lib/coq/tools/coqdoc/coqdoc.css
|
||||
lib/coq/tools/coqdoc/coqdoc.sty
|
||||
lib/coq/toplevel/auto_ind_decl.cmi
|
||||
lib/coq/toplevel/autoinstance.cmi
|
||||
lib/coq/toplevel/cerrors.cmi
|
||||
lib/coq/toplevel/class.cmi
|
||||
lib/coq/toplevel/classes.cmi
|
||||
@ -717,11 +875,13 @@ lib/coq/toplevel/coqtop.cmi
|
||||
lib/coq/toplevel/discharge.cmi
|
||||
lib/coq/toplevel/himsg.cmi
|
||||
lib/coq/toplevel/ind_tables.cmi
|
||||
lib/coq/toplevel/line_oriented_parser.cmi
|
||||
lib/coq/toplevel/indschemes.cmi
|
||||
lib/coq/toplevel/lemmas.cmi
|
||||
lib/coq/toplevel/libtypes.cmi
|
||||
lib/coq/toplevel/metasyntax.cmi
|
||||
lib/coq/toplevel/mltop.cmi
|
||||
lib/coq/toplevel/protectedtoplevel.cmi
|
||||
lib/coq/toplevel/record.cmi
|
||||
lib/coq/toplevel/search.cmi
|
||||
lib/coq/toplevel/toplevel.a
|
||||
lib/coq/toplevel/toplevel.cma
|
||||
lib/coq/toplevel/toplevel.cmi
|
||||
@ -733,29 +893,32 @@ lib/coq/toplevel/vernacexpr.cmi
|
||||
lib/coq/toplevel/vernacinterp.cmi
|
||||
lib/coq/toplevel/whelp.cmi
|
||||
@dirrm lib/coq/config
|
||||
@dirrm lib/coq/contrib/cc
|
||||
@dirrm lib/coq/contrib/dp
|
||||
@dirrm lib/coq/contrib/extraction
|
||||
@dirrm lib/coq/contrib/field
|
||||
@dirrm lib/coq/contrib/firstorder
|
||||
@dirrm lib/coq/contrib/fourier
|
||||
@dirrm lib/coq/contrib/funind
|
||||
@dirrm lib/coq/contrib/interface
|
||||
@dirrm lib/coq/contrib/micromega
|
||||
@dirrm lib/coq/contrib/omega
|
||||
@dirrm lib/coq/contrib/ring
|
||||
@dirrm lib/coq/contrib/romega
|
||||
@dirrm lib/coq/contrib/rtauto
|
||||
@dirrm lib/coq/contrib/setoid_ring
|
||||
@dirrm lib/coq/contrib/subtac
|
||||
@dirrm lib/coq/contrib/xml
|
||||
@dirrm lib/coq/contrib
|
||||
%%IDE%%@dirrm lib/coq/ide
|
||||
@dirrm lib/coq/ide/utils
|
||||
@dirrm lib/coq/ide
|
||||
@dirrm lib/coq/interp
|
||||
@dirrm lib/coq/kernel
|
||||
@dirrm lib/coq/lib
|
||||
@dirrm lib/coq/library
|
||||
@dirrm lib/coq/parsing
|
||||
@dirrm lib/coq/plugins/cc
|
||||
@dirrm lib/coq/plugins/dp
|
||||
@dirrm lib/coq/plugins/extraction
|
||||
@dirrm lib/coq/plugins/field
|
||||
@dirrm lib/coq/plugins/firstorder
|
||||
@dirrm lib/coq/plugins/fourier
|
||||
@dirrm lib/coq/plugins/funind
|
||||
@dirrm lib/coq/plugins/micromega
|
||||
@dirrm lib/coq/plugins/nsatz
|
||||
@dirrm lib/coq/plugins/omega
|
||||
@dirrm lib/coq/plugins/quote
|
||||
@dirrm lib/coq/plugins/ring
|
||||
@dirrm lib/coq/plugins/romega
|
||||
@dirrm lib/coq/plugins/rtauto
|
||||
@dirrm lib/coq/plugins/setoid_ring
|
||||
@dirrm lib/coq/plugins/subtac
|
||||
@dirrm lib/coq/plugins/syntax
|
||||
@dirrm lib/coq/plugins/xml
|
||||
@dirrm lib/coq/plugins
|
||||
@dirrm lib/coq/pretyping
|
||||
@dirrm lib/coq/proofs
|
||||
@dirrm lib/coq/states
|
||||
@ -767,6 +930,7 @@ lib/coq/toplevel/whelp.cmi
|
||||
@dirrm lib/coq/theories/Init
|
||||
@dirrm lib/coq/theories/Lists
|
||||
@dirrm lib/coq/theories/Logic
|
||||
@dirrm lib/coq/theories/MSets
|
||||
@dirrm lib/coq/theories/NArith
|
||||
@dirrm lib/coq/theories/Numbers/Cyclic/Abstract
|
||||
@dirrm lib/coq/theories/Numbers/Cyclic/DoubleCyclic
|
||||
@ -798,6 +962,7 @@ lib/coq/toplevel/whelp.cmi
|
||||
@dirrm lib/coq/theories/Sets
|
||||
@dirrm lib/coq/theories/Sorting
|
||||
@dirrm lib/coq/theories/Strings
|
||||
@dirrm lib/coq/theories/Structures
|
||||
@dirrm lib/coq/theories/Unicode
|
||||
@dirrm lib/coq/theories/Wellfounded
|
||||
@dirrm lib/coq/theories/ZArith
|
||||
@ -807,6 +972,9 @@ lib/coq/toplevel/whelp.cmi
|
||||
@dirrm lib/coq/toplevel
|
||||
@dirrm lib/coq/user-contrib
|
||||
@dirrm lib/coq
|
||||
share/emacs/site-lisp/coq-db.el
|
||||
share/emacs/site-lisp/coq-font-lock.el
|
||||
share/emacs/site-lisp/coq-inferior.el
|
||||
share/emacs/site-lisp/coq-syntax.el
|
||||
share/emacs/site-lisp/coq.el
|
||||
share/emacs/site-lisp/coqdoc.sty
|
||||
|
||||
Loading…
Reference in New Issue
Block a user