This is an automated email from the git hooks/post-receive script. gareuselesinge pushed a change to branch master in repository coq.
from c01be74 update changelog new 0aa2544 Imported Upstream version 8.5~beta2+dfsg new e347929 Merge tag 'upstream/8.5_beta2+dfsg' into test new 9efa102 Remove unneeded comment new b9b5b95 beta2 new 7e60dbc more overrides The 5 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 +- debian/changelog | 7 +- debian/libcoq-ocaml.lintian-overrides | 1 + debian/rules | 5 +- 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 -- 555 files changed, 14751 insertions(+), 4365 deletions(-) delete mode 100644 INSTALL.macosx create mode 100644 debian/libcoq-ocaml.lintian-overrides 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 _______________________________________________ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits