[Pkg-ocaml-maint-commits] [coq] 02/05: Merge tag 'upstream/8.5_beta2+dfsg' into test
Enrico Tassi
gareuselesinge at moszumanska.debian.org
Wed Jul 15 20:12:35 UTC 2015
This is an automated email from the git hooks/post-receive script.
gareuselesinge pushed a commit to branch master
in repository coq.
commit e347929583f820a2cc0296597b6382309e930989
Merge: c01be74 0aa2544
Author: Enrico Tassi <gareuselesinge at debian.org>
Date: Wed Jul 15 13:15:50 2015 +0200
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
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(-)
--
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