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 <gareuselesi...@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 _______________________________________________ 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