[Pkg-ocaml-maint-commits] [coq] branch upstream updated (cec4741 -> 0aa2544)
Enrico Tassi
gareuselesinge at moszumanska.debian.org
Wed Jul 15 20:12:37 UTC 2015
This is an automated email from the git hooks/post-receive script.
gareuselesinge pushed a change to branch upstream
in repository coq.
from cec4741 Imported Upstream version 8.5~beta1+dfsg
new 0aa2544 Imported Upstream version 8.5~beta2+dfsg
The 1 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails. The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.
Summary of changes:
CHANGES | 143 +-
COMPATIBILITY | 14 +
INSTALL | 48 +-
INSTALL.ide | 126 +-
INSTALL.macosx | 20 -
Makefile | 2 +-
Makefile.build | 10 +-
Makefile.common | 12 +-
Makefile.doc | 14 +-
README.win | 49 +-
_tags | 4 +-
checker/check.ml | 2 +-
checker/checker.ml | 3 +-
checker/cic.mli | 2 +-
checker/declarations.ml | 2 +-
checker/indtypes.ml | 1 -
checker/reduction.ml | 10 +-
checker/safe_typing.ml | 3 +-
checker/univ.ml | 43 +-
checker/values.ml | 43 +-
checker/votour.ml | 154 +-
configure.ml | 177 +-
dev/TODO | 22 -
dev/nsis/coq.nsi | 4 +-
dev/top_printers.ml | 5 +-
doc/stdlib/index-list.html.template | 7 +
doc/whodidwhat/whodidwhat-8.4update.tex | 20 +-
grammar/vernacextend.ml4 | 50 +-
ide/MacOS/Info.plist.template | 2 +-
ide/MacOS/default_accel_map | 1 -
ide/coq.lang | 59 +-
ide/coqOps.ml | 42 +-
ide/coq_commands.ml | 2 -
ide/coqide.ml | 73 +-
ide/coqide_ui.ml | 1 -
ide/gtk_parsing.ml | 13 +
ide/ide_slave.ml | 8 +-
ide/ideutils.ml | 50 +-
ide/ideutils.mli | 4 +-
ide/preferences.ml | 39 +-
ide/preferences.mli | 2 +
ide/project_file.ml4 | 22 +-
ide/session.ml | 41 +-
ide/session.mli | 1 +
ide/tags.ml | 26 +-
ide/tags.mli | 13 +-
ide/wg_Find.ml | 14 +-
ide/wg_MessageView.ml | 31 +-
ide/wg_MessageView.mli | 9 +
ide/wg_ProofView.ml | 5 +
ide/wg_ProofView.mli | 1 +
ide/wg_ScriptView.ml | 13 +-
ide/wg_Segment.ml | 31 +-
ide/wg_Segment.mli | 8 +
interp/constrarg.ml | 3 +
interp/constrarg.mli | 2 +
interp/constrextern.ml | 2 +-
interp/constrintern.ml | 1 -
interp/constrintern.mli | 1 +
interp/coqlib.ml | 2 -
interp/coqlib.mli | 1 -
interp/genintern.ml | 1 -
interp/genintern.mli | 1 -
interp/modintern.ml | 4 +-
interp/notation.ml | 32 +-
interp/notation.mli | 4 +
interp/notation_ops.ml | 63 +
interp/notation_ops.mli | 2 +
intf/tacexpr.mli | 2 -
intf/vernacexpr.mli | 4 +-
kernel/byterun/coq_fix_code.c | 11 +-
kernel/byterun/coq_interp.c | 81 +-
kernel/byterun/int64_native.h | 16 +-
kernel/cbytecodes.ml | 3 +
kernel/cbytecodes.mli | 1 +
kernel/cbytegen.ml | 132 +-
kernel/cbytegen.mli | 9 +-
kernel/cemitcodes.ml | 90 +-
kernel/closure.ml | 20 +-
kernel/constr.ml | 95 +-
kernel/constr.mli | 17 +-
kernel/csymtable.ml | 23 +-
kernel/declarations.mli | 8 +-
kernel/declareops.ml | 2 +-
kernel/declareops.mli | 1 -
kernel/environ.ml | 2 +-
kernel/environ.mli | 2 +-
kernel/fast_typeops.mli | 5 -
kernel/indtypes.ml | 21 +-
kernel/inductive.ml | 9 +-
kernel/mod_typing.ml | 27 +-
kernel/modops.ml | 57 +-
kernel/names.ml | 10 +-
kernel/names.mli | 6 +-
kernel/nativecode.ml | 1 -
kernel/nativelambda.ml | 9 +-
kernel/nativelambda.mli | 1 -
kernel/nativelib.ml | 5 +-
kernel/nativelibrary.ml | 1 -
kernel/nativevalues.ml | 12 +-
kernel/opaqueproof.mli | 1 -
kernel/reduction.ml | 8 -
kernel/safe_typing.ml | 6 +-
kernel/term_typing.ml | 17 +-
kernel/term_typing.mli | 1 -
kernel/typeops.ml | 10 +-
kernel/uint31.ml | 4 +-
kernel/uint31.mli | 2 +-
kernel/univ.ml | 47 +-
kernel/vconv.ml | 5 +-
kernel/vm.ml | 18 +-
kernel/vm.mli | 2 +-
lib/cArray.ml | 28 +-
lib/cArray.mli | 5 +
lib/cString.ml | 9 +-
lib/cThread.ml | 41 +-
lib/dyn.ml | 2 +
lib/dyn.mli | 1 +
lib/errors.ml | 2 +-
lib/errors.mli | 2 +-
lib/future.ml | 72 +-
lib/future.mli | 5 +-
lib/hashcons.ml | 3 +
lib/hashcons.mli | 2 +
lib/hashset.ml | 26 +
lib/hashset.mli | 9 +
lib/monad.ml | 2 +-
lib/pp.ml | 13 +-
lib/richpp.ml | 215 +-
lib/richpp.mli | 4 +-
lib/terminal.ml | 3 +-
library/assumptions.ml | 151 +-
library/assumptions.mli | 15 +-
library/declare.ml | 33 +-
library/declare.mli | 2 +-
library/global.mli | 18 +-
library/globnames.ml | 1 -
library/goptions.ml | 10 +-
library/libnames.ml | 5 +
library/libnames.mli | 2 +
library/library.ml | 326 +--
library/library.mli | 15 +-
library/loadpath.ml | 83 +-
library/loadpath.mli | 16 +-
library/states.ml | 1 +
library/states.mli | 1 +
library/summary.ml | 1 +
library/universes.ml | 9 +-
library/universes.mli | 3 -
parsing/g_constr.ml4 | 2 +-
parsing/g_ltac.ml4 | 8 +-
parsing/g_proofs.ml4 | 14 +-
parsing/g_tactic.ml4 | 2 +-
parsing/g_vernac.ml4 | 5 +-
parsing/pcoq.ml4 | 2 +
parsing/pcoq.mli | 2 +
plugins/cc/ccproof.mli | 1 -
plugins/cc/cctac.ml | 20 +-
plugins/decl_mode/decl_expr.mli | 32 +-
plugins/decl_mode/decl_mode.ml | 26 +-
plugins/decl_mode/decl_mode.mli | 4 +-
plugins/decl_mode/decl_proof_instr.ml | 39 +-
plugins/decl_mode/g_decl_mode.ml4 | 57 +-
plugins/decl_mode/ppdecl_proof.ml | 169 +-
plugins/decl_mode/ppdecl_proof.mli | 14 +-
plugins/derive/derive.ml | 4 +-
plugins/extraction/ExtrHaskellBasic.v | 15 +
plugins/extraction/ExtrOcamlNatInt.v | 1 +
plugins/extraction/common.ml | 3 +-
plugins/extraction/extract_env.ml | 6 +-
plugins/extraction/extraction_plugin.mllib | 1 +
plugins/extraction/g_extraction.ml4 | 2 +
plugins/extraction/haskell.ml | 36 +-
plugins/extraction/json.ml | 278 +++
plugins/extraction/json.mli | 1 +
plugins/extraction/miniml.mli | 1 +
plugins/extraction/ocaml.ml | 15 +-
plugins/extraction/scheme.ml | 3 +-
plugins/extraction/table.ml | 2 +-
plugins/extraction/table.mli | 2 +-
plugins/extraction/vo.itarget | 1 +
plugins/firstorder/formula.mli | 1 -
plugins/firstorder/instances.ml | 32 +-
plugins/firstorder/sequent.ml | 2 +-
plugins/fourier/fourierR.ml | 1 -
plugins/funind/functional_principles_proofs.ml | 123 +-
plugins/funind/functional_principles_proofs.mli | 1 +
plugins/funind/functional_principles_types.ml | 143 +-
plugins/funind/functional_principles_types.mli | 6 +-
plugins/funind/g_indfun.ml4 | 6 +-
plugins/funind/glob_term_to_relation.ml | 54 +-
plugins/funind/glob_term_to_relation.mli | 7 +-
plugins/funind/indfun.ml | 221 +-
plugins/funind/indfun_common.ml | 6 +-
plugins/funind/indfun_common.mli | 2 +-
plugins/funind/invfun.ml | 517 ++---
plugins/funind/recdef.ml | 118 +-
plugins/micromega/MExtraction.v | 2 +-
plugins/omega/Omega.v | 8 +-
plugins/omega/OmegaPlugin.v | 6 +
toplevel/whelp.mli => plugins/omega/OmegaTactic.v | 15 +-
plugins/omega/vo.itarget | 1 +
plugins/quote/quote.ml | 4 +-
pretyping/cases.ml | 33 +-
pretyping/classops.ml | 6 +-
pretyping/constr_matching.ml | 74 +-
pretyping/detyping.ml | 11 +-
pretyping/evarconv.ml | 26 +-
pretyping/evarsolve.ml | 163 +-
pretyping/evarutil.ml | 13 +-
pretyping/evarutil.mli | 10 +
pretyping/evd.ml | 55 +-
pretyping/evd.mli | 14 +-
pretyping/find_subterm.ml | 1 -
pretyping/find_subterm.mli | 1 -
pretyping/glob_ops.mli | 3 +
pretyping/inductiveops.ml | 21 +-
pretyping/inductiveops.mli | 10 +-
pretyping/patternops.ml | 52 +-
pretyping/patternops.mli | 3 +-
pretyping/pretyping.ml | 10 +-
pretyping/pretyping.mli | 2 +-
pretyping/reductionops.ml | 52 +-
pretyping/reductionops.mli | 7 +-
pretyping/retyping.ml | 5 +-
pretyping/tacred.ml | 14 +-
pretyping/termops.ml | 1 -
pretyping/termops.mli | 1 -
pretyping/typeclasses.ml | 11 -
pretyping/typeclasses.mli | 2 -
pretyping/typeclasses_errors.ml | 1 -
pretyping/typeclasses_errors.mli | 1 -
pretyping/typing.mli | 1 -
pretyping/unification.ml | 13 +-
pretyping/vnorm.ml | 17 +-
printing/ppconstrsig.mli | 2 -
printing/pptactic.mli | 5 +-
printing/pptacticsig.mli | 1 -
printing/ppvernac.ml | 17 +-
printing/prettyp.ml | 14 +-
printing/printer.ml | 61 +-
printing/printer.mli | 6 +-
printing/richprinter.ml | 7 +-
printing/richprinter.mli | 4 +-
proofs/clenv.mli | 1 -
proofs/clenvtac.mli | 1 -
proofs/goal.ml | 2 -
proofs/logic.ml | 12 -
proofs/pfedit.ml | 35 +
proofs/pfedit.mli | 8 +
proofs/proof.mli | 2 +-
proofs/proof_global.ml | 32 +-
proofs/proof_global.mli | 6 +-
proofs/proof_type.ml | 1 -
proofs/proof_type.mli | 1 -
proofs/proofview.ml | 72 +-
proofs/proofview.mli | 10 +-
proofs/redexpr.ml | 2 +-
stm/asyncTaskQueue.ml | 4 +-
stm/asyncTaskQueue.mli | 2 +
stm/lemmas.ml | 101 +-
stm/lemmas.mli | 1 -
stm/spawned.ml | 5 +-
stm/stm.ml | 396 ++--
stm/tQueue.ml | 2 +-
stm/tQueue.mli | 4 +-
stm/texmacspp.ml | 31 +-
stm/vernac_classifier.ml | 7 +-
stm/vio_checking.ml | 2 +-
tactics/auto.ml | 5 +-
tactics/auto.mli | 1 -
tactics/autorewrite.ml | 1 +
tactics/btermdn.ml | 2 +-
tactics/btermdn.mli | 2 +-
tactics/class_tactics.ml | 32 +-
tactics/contradiction.ml | 2 -
tactics/coretactics.ml4 | 30 +-
tactics/dn.ml | 2 +-
tactics/dn.mli | 2 +-
tactics/dnet.ml | 14 +-
tactics/dnet.mli | 2 +
tactics/eauto.ml4 | 94 +-
tactics/eauto.mli | 1 -
tactics/elim.ml | 1 -
tactics/equality.ml | 18 +-
tactics/equality.mli | 1 -
tactics/evar_tactics.ml | 7 +-
tactics/evar_tactics.mli | 1 -
tactics/extratactics.ml4 | 30 +-
tactics/hints.ml | 227 +-
tactics/hints.mli | 20 +-
tactics/hipattern.mli | 3 -
tactics/inv.mli | 1 -
tactics/leminv.ml | 14 +-
tactics/leminv.mli | 1 -
tactics/rewrite.ml | 47 +-
tactics/taccoerce.ml | 7 +
tactics/tacenv.ml | 2 -
tactics/tacintern.ml | 12 +-
tactics/tacintern.mli | 1 -
tactics/tacinterp.ml | 183 +-
tactics/tacsubst.ml | 14 +-
tactics/tacticals.ml | 24 +-
tactics/tacticals.mli | 4 +-
tactics/tactics.ml | 110 +-
tactics/tactics.mli | 5 +-
tactics/term_dnet.ml | 12 +
tactics/term_dnet.mli | 2 +
test-suite/Makefile | 1 +
test-suite/_CoqProject | 1 +
test-suite/bugs/closed/1704.v | 1 +
test-suite/bugs/closed/2378.v | 1 +
test-suite/bugs/closed/2406.v | 2 +-
test-suite/bugs/closed/2473.v | 1 +
test-suite/bugs/closed/2590.v | 20 +
test-suite/bugs/closed/2602.v | 8 +
test-suite/bugs/closed/2613.v | 1 +
test-suite/bugs/closed/2615.v | 1 +
test-suite/bugs/closed/2775.v | 6 +
test-suite/bugs/closed/2830.v | 1 +
test-suite/bugs/closed/2883.v | 1 +
test-suite/bugs/closed/2946.v | 8 +
test-suite/bugs/closed/2951.v | 2 +
test-suite/bugs/closed/2969.v | 1 +
test-suite/bugs/closed/2996.v | 1 +
test-suite/bugs/closed/3068.v | 1 +
test-suite/bugs/{opened => closed}/3071.v | 2 +-
test-suite/bugs/closed/3199.v | 18 +
test-suite/bugs/closed/3210.v | 22 +
test-suite/bugs/closed/3249.v | 11 +
test-suite/bugs/closed/3258.v | 1 +
test-suite/bugs/closed/3259.v | 1 +
test-suite/bugs/{opened => closed}/3298.v | 7 +-
test-suite/bugs/closed/3309.v | 10 +-
test-suite/bugs/closed/3314.v | 1 +
test-suite/bugs/closed/3319.v | 1 +
test-suite/bugs/closed/3321.v | 1 +
test-suite/bugs/closed/3322.v | 1 +
test-suite/bugs/closed/3323.v | 1 +
test-suite/bugs/closed/3324.v | 1 +
test-suite/bugs/closed/3329.v | 1 +
test-suite/bugs/closed/3330.v | 1 +
test-suite/bugs/closed/3344.v | 1 +
test-suite/bugs/closed/3347.v | 1 +
test-suite/bugs/closed/3350.v | 1 +
test-suite/bugs/closed/3373.v | 1 +
test-suite/bugs/closed/3374.v | 1 +
test-suite/bugs/closed/3375.v | 1 +
test-suite/bugs/closed/3382.v | 1 +
test-suite/bugs/closed/3392.v | 8 +-
test-suite/bugs/closed/3393.v | 1 +
test-suite/bugs/closed/3422.v | 1 +
test-suite/bugs/closed/3427.v | 1 +
test-suite/bugs/closed/3439.v | 1 +
test-suite/bugs/{opened => closed}/3467.v | 2 +-
test-suite/bugs/closed/3480.v | 1 +
test-suite/bugs/closed/3484.v | 1 +
test-suite/bugs/{opened => closed}/3490.v | 0
test-suite/bugs/closed/3491.v | 4 +
test-suite/bugs/closed/3513.v | 76 +
test-suite/bugs/closed/3531.v | 1 +
test-suite/bugs/closed/3560.v | 15 +
test-suite/bugs/closed/3561.v | 1 +
test-suite/bugs/closed/3590.v | 12 +
test-suite/bugs/closed/3596.v | 1 +
test-suite/bugs/closed/3612.v | 47 +
test-suite/bugs/closed/3625.v | 1 +
test-suite/bugs/closed/3647.v | 1 +
test-suite/bugs/closed/3649.v | 57 +
test-suite/bugs/closed/3653.v | 1 +
test-suite/bugs/closed/3658.v | 1 +
test-suite/bugs/closed/3660.v | 1 +
test-suite/bugs/closed/3664.v | 1 +
test-suite/bugs/closed/3668.v | 1 +
test-suite/bugs/{opened => closed}/3681.v | 0
test-suite/bugs/closed/3682.v | 1 +
test-suite/bugs/closed/3684.v | 1 +
test-suite/bugs/closed/3686.v | 1 +
test-suite/bugs/closed/3690.v | 52 +
test-suite/bugs/closed/3698.v | 1 +
test-suite/bugs/closed/3699.v | 1 +
test-suite/bugs/closed/3703.v | 32 +
test-suite/bugs/closed/3709.v | 1 +
test-suite/bugs/closed/3732.v | 105 +
test-suite/bugs/closed/3755.v | 16 +
test-suite/bugs/closed/3782.v | 1 +
test-suite/bugs/closed/3783.v | 33 +
test-suite/bugs/{opened => closed}/3786.v | 13 +-
test-suite/bugs/closed/3798.v | 12 +
test-suite/bugs/closed/3808.v | 2 +
test-suite/bugs/closed/3815.v | 9 +
test-suite/bugs/closed/3854.v | 1 +
test-suite/bugs/closed/3881.v | 35 +
test-suite/bugs/closed/3900.v | 13 +
test-suite/bugs/closed/3916.v | 3 +
test-suite/bugs/closed/3922.v | 84 +
test-suite/bugs/closed/3938.v | 8 +
test-suite/bugs/closed/3944.v | 5 +
test-suite/bugs/closed/3953.v | 5 +
test-suite/bugs/closed/3960.v | 26 +
test-suite/bugs/closed/3978.v | 27 +
test-suite/bugs/closed/3993.v | 3 +
test-suite/bugs/closed/4001.v | 18 +
test-suite/bugs/closed/4012.v | 5 +
test-suite/bugs/closed/4016.v | 12 +
test-suite/bugs/closed/4017.v | 8 +
test-suite/bugs/closed/4018.v | 3 +
test-suite/bugs/closed/4031.v | 14 +
test-suite/bugs/closed/4035.v | 13 +
test-suite/bugs/closed/4046.v | 6 +
test-suite/bugs/closed/4078.v | 14 +
test-suite/bugs/closed/4089.v | 374 ++++
test-suite/bugs/closed/4097.v | 65 +
test-suite/bugs/closed/4101.v | 19 +
test-suite/bugs/closed/4103.v | 12 +
test-suite/bugs/closed/4120.v | 5 +
test-suite/bugs/closed/4121.v | 15 +
test-suite/bugs/closed/4165.v | 7 +
test-suite/bugs/closed/4190.v | 15 +
test-suite/bugs/closed/4193.v | 7 +
test-suite/bugs/closed/HoTT_coq_007.v | 1 +
test-suite/bugs/closed/HoTT_coq_014.v | 2 +
test-suite/bugs/closed/HoTT_coq_020.v | 1 +
test-suite/bugs/closed/HoTT_coq_029.v | 1 +
test-suite/bugs/closed/HoTT_coq_030.v | 1 +
test-suite/bugs/closed/HoTT_coq_035.v | 1 +
test-suite/bugs/closed/HoTT_coq_042.v | 1 +
test-suite/bugs/closed/HoTT_coq_055.v | 1 +
test-suite/bugs/closed/HoTT_coq_056.v | 1 +
test-suite/bugs/closed/HoTT_coq_058.v | 1 +
test-suite/bugs/closed/HoTT_coq_061.v | 1 +
test-suite/bugs/closed/HoTT_coq_062.v | 1 +
test-suite/bugs/closed/HoTT_coq_064.v | 1 +
test-suite/bugs/closed/HoTT_coq_067.v | 1 +
test-suite/bugs/closed/HoTT_coq_088.v | 1 +
test-suite/bugs/closed/HoTT_coq_090.v | 1 +
test-suite/bugs/closed/HoTT_coq_098.v | 1 +
test-suite/bugs/closed/HoTT_coq_099.v | 1 +
test-suite/bugs/closed/HoTT_coq_100.v | 1 +
test-suite/bugs/closed/HoTT_coq_101.v | 1 +
test-suite/bugs/closed/HoTT_coq_102.v | 1 +
test-suite/bugs/closed/HoTT_coq_107.v | 6 +-
test-suite/bugs/closed/HoTT_coq_108.v | 1 +
test-suite/bugs/closed/HoTT_coq_112.v | 1 +
test-suite/bugs/closed/HoTT_coq_113.v | 1 +
test-suite/bugs/closed/HoTT_coq_118.v | 1 +
test-suite/bugs/closed/HoTT_coq_121.v | 1 +
test-suite/bugs/closed/HoTT_coq_123.v | 1 +
test-suite/bugs/{closed => opened}/2456.v | 4 +-
test-suite/bugs/opened/2951.v | 1 -
test-suite/bugs/opened/3263.v | 1 +
test-suite/bugs/opened/3345.v | 1 +
test-suite/bugs/opened/3395.v | 1 +
test-suite/bugs/opened/3491.v | 2 -
test-suite/bugs/opened/3509.v | 1 +
test-suite/bugs/opened/3510.v | 1 +
test-suite/bugs/{closed => opened}/3593.v | 2 +-
test-suite/bugs/opened/3685.v | 1 +
test-suite/bugs/opened/3754.v | 1 +
test-suite/bugs/opened/3794.v | 7 +
test-suite/bugs/{closed => opened}/3848.v | 3 +-
test-suite/bugs/opened/HoTT_coq_120.v | 1 +
test-suite/complexity/bug4076.v | 29 +
test-suite/complexity/bug4076bis.v | 31 +
test-suite/ide/undo020.fake | 4 +-
test-suite/output/Arguments.out | 17 +-
test-suite/output/ArgumentsScope.out | 14 -
test-suite/output/Arguments_renaming.out | 23 +-
test-suite/output/Cases.out | 9 -
test-suite/output/Errors.out | 8 +-
test-suite/output/Implicit.out | 1 -
test-suite/output/Notations.out | 22 +-
test-suite/output/PrintInfos.out | 9 -
test-suite/output/TranspModtype.out | 8 -
test-suite/output/inference.out | 2 -
test-suite/output/names.out | 1 -
test-suite/output/rewrite-2172.out | 2 +-
test-suite/output/simpl.v | 6 +-
test-suite/prerequisite/admit.v | 2 +
test-suite/success/AdvancedCanonicalStructure.v | 1 +
test-suite/success/Case22.v | 12 +
test-suite/success/Inductive.v | 41 +
test-suite/success/Injection.v | 2 +
test-suite/success/Nsatz.v | 1 +
test-suite/success/TacticNotation1.v | 20 +
test-suite/success/apply.v | 10 +
test-suite/success/coindprim.v | 52 +
test-suite/success/proof_using.v | 1 +
test-suite/success/qed_export.v | 18 +
test-suite/success/rewrite.v | 10 +
test-suite/success/rewrite_dep.v | 1 +
test-suite/success/setoid_test.v | 1 +
test-suite/success/simpl.v | 1 +
test-suite/success/tryif.v | 50 +
theories/Classes/CMorphisms.v | 24 +-
theories/Init/Logic.v | 3 -
theories/Init/Notations.v | 2 +-
theories/Init/Prelude.v | 2 +-
theories/Init/Tactics.v | 14 +-
theories/Lists/List.v | 10 +-
theories/Lists/SetoidList.v | 11 +-
theories/Lists/SetoidPermutation.v | 74 +-
theories/MMaps/MMapAVL.v | 2158 ++++++++++++++++++
theories/MMaps/MMapFacts.v | 2434 +++++++++++++++++++++
theories/MMaps/MMapInterface.v | 292 +++
theories/MMaps/MMapList.v | 1144 ++++++++++
theories/MMaps/MMapPositive.v | 698 ++++++
theories/MMaps/MMapWeakList.v | 687 ++++++
lib/dyn.mli => theories/MMaps/MMaps.v | 28 +-
theories/MMaps/vo.itarget | 7 +
theories/MSets/MSetAVL.v | 18 +-
theories/MSets/MSetPositive.v | 81 +-
theories/Program/Equality.v | 11 +-
theories/Program/Utils.v | 2 +-
theories/Reals/Alembert.v | 1 +
theories/Reals/Cos_rel.v | 7 +-
theories/Reals/PSeries_reg.v | 6 +
theories/Reals/Ratan.v | 10 +
theories/Structures/EqualitiesFacts.v | 216 +-
theories/Structures/OrdersEx.v | 67 +
theories/Structures/OrdersLists.v | 211 +-
theories/ZArith/Int.v | 193 +-
theories/theories.itarget | 1 +
tools/coq_makefile.ml | 80 +-
tools/coq_tex.ml | 3 +-
tools/coqc.ml | 4 +-
tools/coqdoc/cpretty.mll | 12 +-
tools/coqdoc/output.ml | 1 -
toplevel/auto_ind_decl.mli | 1 -
toplevel/cerrors.ml | 46 +-
toplevel/cerrors.mli | 2 +-
toplevel/classes.ml | 15 +-
toplevel/classes.mli | 3 +-
toplevel/command.ml | 19 +-
toplevel/command.mli | 3 +-
toplevel/coqinit.ml | 33 +-
toplevel/coqinit.mli | 4 +-
toplevel/coqtop.ml | 18 +-
toplevel/himsg.ml | 4 +-
toplevel/indschemes.ml | 2 +-
toplevel/metasyntax.ml | 33 +-
toplevel/mltop.ml | 19 +-
toplevel/mltop.mli | 1 -
toplevel/obligations.ml | 24 +-
toplevel/obligations.mli | 7 +-
toplevel/record.ml | 7 +-
toplevel/toplevel.mllib | 1 -
toplevel/usage.ml | 10 +-
toplevel/vernacentries.ml | 98 +-
toplevel/vernacinterp.ml | 22 +-
toplevel/vernacinterp.mli | 8 +-
toplevel/whelp.ml4 | 224 --
552 files changed, 14745 insertions(+), 4358 deletions(-)
delete mode 100644 INSTALL.macosx
delete mode 100644 dev/TODO
create mode 100644 plugins/extraction/ExtrHaskellBasic.v
create mode 100644 plugins/extraction/json.ml
create mode 100644 plugins/extraction/json.mli
rename toplevel/whelp.mli => plugins/omega/OmegaTactic.v (68%)
create mode 100644 test-suite/_CoqProject
create mode 100644 test-suite/bugs/closed/2590.v
create mode 100644 test-suite/bugs/closed/2602.v
create mode 100644 test-suite/bugs/closed/2775.v
create mode 100644 test-suite/bugs/closed/2946.v
create mode 100644 test-suite/bugs/closed/2951.v
rename test-suite/bugs/{opened => closed}/3071.v (82%)
create mode 100644 test-suite/bugs/closed/3199.v
create mode 100644 test-suite/bugs/closed/3210.v
create mode 100644 test-suite/bugs/closed/3249.v
rename test-suite/bugs/{opened => closed}/3298.v (79%)
rename test-suite/bugs/{opened => closed}/3467.v (78%)
rename test-suite/bugs/{opened => closed}/3490.v (100%)
create mode 100644 test-suite/bugs/closed/3491.v
create mode 100644 test-suite/bugs/closed/3513.v
create mode 100644 test-suite/bugs/closed/3560.v
create mode 100644 test-suite/bugs/closed/3590.v
create mode 100644 test-suite/bugs/closed/3612.v
create mode 100644 test-suite/bugs/closed/3649.v
rename test-suite/bugs/{opened => closed}/3681.v (100%)
create mode 100644 test-suite/bugs/closed/3690.v
create mode 100644 test-suite/bugs/closed/3703.v
create mode 100644 test-suite/bugs/closed/3732.v
create mode 100644 test-suite/bugs/closed/3755.v
create mode 100644 test-suite/bugs/closed/3783.v
rename test-suite/bugs/{opened => closed}/3786.v (80%)
create mode 100644 test-suite/bugs/closed/3798.v
create mode 100644 test-suite/bugs/closed/3808.v
create mode 100644 test-suite/bugs/closed/3815.v
create mode 100644 test-suite/bugs/closed/3881.v
create mode 100644 test-suite/bugs/closed/3900.v
create mode 100644 test-suite/bugs/closed/3916.v
create mode 100644 test-suite/bugs/closed/3922.v
create mode 100644 test-suite/bugs/closed/3938.v
create mode 100644 test-suite/bugs/closed/3944.v
create mode 100644 test-suite/bugs/closed/3953.v
create mode 100644 test-suite/bugs/closed/3960.v
create mode 100644 test-suite/bugs/closed/3978.v
create mode 100644 test-suite/bugs/closed/3993.v
create mode 100644 test-suite/bugs/closed/4001.v
create mode 100644 test-suite/bugs/closed/4012.v
create mode 100644 test-suite/bugs/closed/4016.v
create mode 100644 test-suite/bugs/closed/4017.v
create mode 100644 test-suite/bugs/closed/4018.v
create mode 100644 test-suite/bugs/closed/4031.v
create mode 100644 test-suite/bugs/closed/4035.v
create mode 100644 test-suite/bugs/closed/4046.v
create mode 100644 test-suite/bugs/closed/4078.v
create mode 100644 test-suite/bugs/closed/4089.v
create mode 100644 test-suite/bugs/closed/4097.v
create mode 100644 test-suite/bugs/closed/4101.v
create mode 100644 test-suite/bugs/closed/4103.v
create mode 100644 test-suite/bugs/closed/4120.v
create mode 100644 test-suite/bugs/closed/4121.v
create mode 100644 test-suite/bugs/closed/4165.v
create mode 100644 test-suite/bugs/closed/4190.v
create mode 100644 test-suite/bugs/closed/4193.v
rename test-suite/bugs/{closed => opened}/2456.v (97%)
delete mode 100644 test-suite/bugs/opened/2951.v
delete mode 100644 test-suite/bugs/opened/3491.v
rename test-suite/bugs/{closed => opened}/3593.v (77%)
create mode 100644 test-suite/bugs/opened/3794.v
rename test-suite/bugs/{closed => opened}/3848.v (91%)
create mode 100644 test-suite/complexity/bug4076.v
create mode 100644 test-suite/complexity/bug4076bis.v
create mode 100644 test-suite/prerequisite/admit.v
create mode 100644 test-suite/success/TacticNotation1.v
create mode 100644 test-suite/success/coindprim.v
create mode 100644 test-suite/success/qed_export.v
create mode 100644 test-suite/success/tryif.v
create mode 100644 theories/MMaps/MMapAVL.v
create mode 100644 theories/MMaps/MMapFacts.v
create mode 100644 theories/MMaps/MMapInterface.v
create mode 100644 theories/MMaps/MMapList.v
create mode 100644 theories/MMaps/MMapPositive.v
create mode 100644 theories/MMaps/MMapWeakList.v
copy lib/dyn.mli => theories/MMaps/MMaps.v (53%)
create mode 100644 theories/MMaps/vo.itarget
delete mode 100644 toplevel/whelp.ml4
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git
More information about the Pkg-ocaml-maint-commits
mailing list