This is an automated email from the git hooks/post-receive script. gareuselesinge pushed a commit to branch master in repository coq.
commit 4e76c4f01b69b77f40686e06c4544aa156efaa5a Merge: 64fa31c 91dbeab Author: Enrico Tassi <gareuselesi...@debian.org> Date: Fri Nov 13 11:43:34 2015 +0100 Imported Upstream version 8.5~beta3+dfsg .gitattributes | 5 + .mailmap | 89 +++++ CHANGES | 134 ++++++- INSTALL | 10 +- INSTALL.doc | 28 +- INSTALL.ide | 2 +- Makefile | 3 +- Makefile.build | 22 +- Makefile.common | 13 +- Makefile.doc | 26 +- README.doc | 0 checker/analyze.ml | 350 ++++++++++++++++++ checker/analyze.mli | 35 ++ checker/check.ml | 53 ++- checker/check.mllib | 4 +- checker/check_stat.ml | 18 +- checker/checker.ml | 34 +- checker/cic.mli | 21 +- checker/closure.ml | 11 +- checker/closure.mli | 4 +- checker/declarations.ml | 19 +- checker/declarations.mli | 5 +- checker/environ.ml | 48 ++- checker/environ.mli | 8 +- checker/indtypes.ml | 12 +- checker/inductive.ml | 92 ++--- checker/mod_checking.ml | 22 +- checker/modops.ml | 7 +- checker/print.ml | 2 +- checker/reduction.ml | 15 +- checker/safe_typing.ml | 30 +- checker/safe_typing.mli | 4 +- checker/term.ml | 2 +- checker/typeops.ml | 2 +- checker/univ.ml | 87 +++-- checker/univ.mli | 20 +- checker/values.ml | 26 +- checker/votour.ml | 140 ++++++- configure.ml | 46 ++- dev/TODO | 22 ++ dev/base_include | 2 + dev/doc/README-V1-V5 | 293 +++++++++++++++ dev/doc/univpoly.txt | 50 ++- dev/doc/versions-history.tex | 109 +++++- dev/make-installer-win32.sh | 4 +- ...-installer-win32.sh => make-installer-win64.sh} | 12 +- dev/nsis/coq.nsi | 4 +- dev/printers.mllib | 6 +- dev/top_printers.ml | 5 + dev/v8-syntax/memo-v8.tex | 2 +- dev/vm_printers.ml | 10 +- doc/stdlib/Library.tex | 0 doc/stdlib/index-list.html.template | 10 +- grammar/grammar.mllib | 5 +- grammar/tacextend.ml4 | 12 +- grammar/vernacextend.ml4 | 2 + ide/config_lexer.mll | 2 +- ide/coq-ssreflect.lang | 1 + ide/coq.lang | 363 ++++++++++--------- ide/coq.mli | 6 +- ide/coqOps.ml | 11 +- ide/coqide.ml | 12 +- ide/ide_slave.ml | 18 +- ide/ideutils.ml | 2 +- ide/interface.mli | 1 + ide/preferences.ml | 33 +- ide/session.ml | 20 +- ide/utf8_convert.mll | 2 +- ide/wg_ProofView.ml | 23 +- ide/wg_ScriptView.ml | 2 +- ide/xmlprotocol.ml | 4 + interp/constrintern.ml | 21 +- interp/constrintern.mli | 10 +- interp/coqlib.ml | 11 +- interp/implicit_quantifiers.ml | 16 +- interp/implicit_quantifiers.mli | 6 +- interp/modintern.ml | 2 +- interp/notation.ml | 41 ++- interp/notation.mli | 1 + interp/syntax_def.ml | 2 +- intf/misctypes.mli | 4 +- intf/tacexpr.mli | 10 +- intf/vernacexpr.mli | 48 ++- kernel/byterun/coq_fix_code.c | 2 +- kernel/byterun/coq_gc.h | 13 +- kernel/byterun/coq_instruct.h | 1 + kernel/byterun/coq_interp.c | 79 +++- kernel/byterun/coq_memory.c | 16 - kernel/byterun/coq_values.c | 1 - kernel/byterun/coq_values.h | 19 +- kernel/cbytecodes.ml | 251 +++++++------ kernel/cbytecodes.mli | 71 ++-- kernel/cbytegen.ml | 266 ++++++++++---- kernel/cbytegen.mli | 10 +- kernel/cemitcodes.ml | 35 +- kernel/cemitcodes.mli | 4 +- kernel/constr.ml | 54 ++- kernel/constr.mli | 20 +- kernel/conv_oracle.ml | 15 +- kernel/csymtable.ml | 44 ++- kernel/declarations.mli | 21 +- kernel/declareops.ml | 18 +- kernel/declareops.mli | 12 +- kernel/entries.mli | 25 +- kernel/environ.ml | 59 +-- kernel/environ.mli | 13 +- kernel/fast_typeops.ml | 8 +- kernel/indtypes.ml | 109 +++--- kernel/indtypes.mli | 2 +- kernel/inductive.ml | 105 +++--- kernel/mod_subst.ml | 2 +- kernel/mod_subst.mli | 5 +- kernel/mod_typing.ml | 119 ++++-- kernel/mod_typing.mli | 13 +- kernel/modops.ml | 12 +- kernel/modops.mli | 3 - kernel/names.ml | 36 +- kernel/names.mli | 4 + kernel/nativecode.ml | 32 +- kernel/nativecode.mli | 26 +- kernel/nativeconv.ml | 136 ++++--- kernel/nativeconv.mli | 4 + kernel/nativelambda.ml | 38 +- kernel/nativelambda.mli | 2 +- kernel/nativelib.ml | 28 +- kernel/nativelibrary.ml | 4 +- kernel/nativelibrary.mli | 2 +- kernel/nativevalues.ml | 2 +- kernel/opaqueproof.ml | 5 +- kernel/pre_env.ml | 6 +- kernel/pre_env.mli | 3 +- kernel/reduction.ml | 58 +-- kernel/reduction.mli | 27 +- kernel/safe_typing.ml | 278 ++++++++------ kernel/safe_typing.mli | 61 +++- kernel/sorts.ml | 10 +- kernel/subtyping.ml | 13 +- kernel/term.ml | 28 +- kernel/term.mli | 31 +- kernel/term_typing.ml | 302 ++++++++++++--- kernel/term_typing.mli | 41 ++- kernel/typeops.ml | 26 +- kernel/univ.ml | 235 ++++++------ kernel/univ.mli | 21 +- kernel/vars.ml | 4 +- kernel/vars.mli | 2 +- kernel/vconv.ml | 191 ++++------ kernel/vconv.mli | 10 +- kernel/vm.ml | 305 +++++++++------- kernel/vm.mli | 25 +- lib/aux_file.ml | 2 + lib/aux_file.mli | 4 + lib/cThread.ml | 14 +- lib/clib.mllib | 1 + lib/dyn.ml | 9 +- lib/errors.ml | 27 +- lib/errors.mli | 10 + lib/flags.ml | 12 +- lib/flags.mli | 13 +- lib/future.ml | 20 +- lib/future.mli | 7 +- lib/pp.ml | 77 ++-- lib/pp.mli | 5 +- lib/pp_control.ml | 11 +- {printing => lib}/ppstyle.ml | 0 {printing => lib}/ppstyle.mli | 0 lib/richpp.mli | 2 +- lib/spawn.ml | 44 ++- lib/system.ml | 79 ++-- lib/system.mli | 10 +- lib/terminal.ml | 7 +- lib/terminal.mli | 3 + lib/util.ml | 11 + lib/util.mli | 3 + lib/xml_lexer.mll | 17 +- lib/xml_parser.mli | 16 +- lib/xml_printer.ml | 2 + library/declare.ml | 261 +++++++------ library/declare.mli | 23 +- library/declaremods.ml | 18 +- library/declaremods.mli | 2 +- library/global.ml | 14 +- library/global.mli | 15 +- library/goptions.ml | 25 +- library/goptions.mli | 2 + library/heads.ml | 5 +- library/impargs.ml | 9 +- library/impargs.mli | 4 +- library/lib.ml | 52 ++- library/lib.mli | 3 +- library/libobject.ml | 16 +- library/library.ml | 185 ++++------ library/library.mli | 17 +- library/library.mllib | 1 - library/loadpath.ml | 8 +- library/loadpath.mli | 7 +- library/nameops.ml | 5 + library/nameops.mli | 2 +- library/nametab.ml | 3 +- library/states.ml | 18 +- library/universes.ml | 221 +++++++---- library/universes.mli | 19 + man/coqide.1 | 20 +- man/coqtop.1 | 19 +- parsing/g_constr.ml4 | 44 ++- parsing/g_proofs.ml4 | 12 +- parsing/g_tactic.ml4 | 66 ++-- parsing/g_vernac.ml4 | 115 ++++-- parsing/g_xml.ml4 | 290 --------------- parsing/lexer.ml4 | 2 +- parsing/pcoq.ml4 | 10 +- plugins/btauto/Algebra.v | 2 +- plugins/cc/ccalgo.ml | 20 +- plugins/cc/ccalgo.mli | 2 +- plugins/cc/cctac.ml | 49 ++- plugins/decl_mode/decl_proof_instr.ml | 42 ++- plugins/derive/derive.ml | 4 +- plugins/extraction/CHANGES | 6 +- plugins/extraction/ExtrHaskellNatInt.v | 13 + plugins/extraction/ExtrHaskellNatInteger.v | 13 + plugins/extraction/ExtrHaskellNatNum.v | 35 ++ plugins/extraction/ExtrHaskellString.v | 38 ++ plugins/extraction/ExtrHaskellZInt.v | 24 ++ plugins/extraction/ExtrHaskellZInteger.v | 23 ++ plugins/extraction/ExtrHaskellZNum.v | 21 ++ plugins/extraction/extraction.ml | 3 +- plugins/extraction/mlutil.ml | 14 +- plugins/extraction/vo.itarget | 9 +- plugins/firstorder/instances.ml | 4 +- plugins/firstorder/sequent.ml | 7 +- plugins/funind/functional_principles_proofs.ml | 24 +- plugins/funind/functional_principles_types.ml | 68 ++-- plugins/funind/functional_principles_types.mli | 10 +- plugins/funind/g_indfun.ml4 | 244 ------------- plugins/funind/glob_term_to_relation.ml | 99 ++--- plugins/funind/glob_termops.mli | 4 +- plugins/funind/indfun.ml | 75 ++-- plugins/funind/indfun_common.ml | 13 +- plugins/funind/indfun_common.mli | 4 +- plugins/funind/invfun.ml | 26 +- plugins/funind/merge.ml | 8 +- plugins/funind/recdef.ml | 32 +- plugins/micromega/mfourier.ml | 2 +- plugins/omega/coq_omega.ml | 10 +- plugins/romega/refl_omega.ml | 8 +- plugins/setoid_ring/newring.ml4 | 13 +- pretyping/cases.ml | 70 ++-- pretyping/classops.mli | 4 +- pretyping/coercion.ml | 28 +- pretyping/constr_matching.ml | 192 +++++----- pretyping/constr_matching.mli | 9 +- pretyping/detyping.ml | 9 +- pretyping/evarconv.ml | 20 +- pretyping/evarsolve.ml | 111 ++++-- pretyping/evarutil.ml | 37 +- pretyping/evarutil.mli | 7 + pretyping/evd.ml | 331 +++++++++++------ pretyping/evd.mli | 57 ++- pretyping/glob_ops.ml | 111 ++++-- pretyping/glob_ops.mli | 1 + pretyping/inductiveops.ml | 12 +- pretyping/inductiveops.mli | 2 + pretyping/miscops.ml | 2 +- pretyping/namegen.ml | 1 + pretyping/nativenorm.ml | 46 ++- pretyping/nativenorm.mli | 6 +- pretyping/patternops.ml | 4 +- pretyping/pretyping.ml | 168 ++++++--- pretyping/pretyping.mli | 28 +- pretyping/pretyping.mllib | 2 +- pretyping/recordops.ml | 2 +- pretyping/reductionops.ml | 26 +- pretyping/reductionops.mli | 18 +- pretyping/retyping.ml | 13 +- pretyping/tacred.ml | 8 +- pretyping/termops.ml | 17 +- pretyping/termops.mli | 4 + pretyping/typeclasses.ml | 2 +- pretyping/typing.ml | 13 +- pretyping/typing.mli | 9 +- pretyping/unification.ml | 13 +- pretyping/vnorm.ml | 106 ++++-- pretyping/vnorm.mli | 2 +- printing/ppconstr.ml | 14 +- printing/pptactic.ml | 9 +- printing/ppvernac.ml | 61 +++- printing/prettyp.ml | 68 ++-- printing/printer.ml | 99 ++++- printing/printer.mli | 22 +- printing/printing.mllib | 1 - printing/printmod.ml | 58 ++- proofs/clenv.ml | 2 +- proofs/clenvtac.ml | 4 +- proofs/evar_refiner.ml | 5 +- proofs/logic.ml | 32 +- proofs/logic_monad.ml | 133 ++++--- proofs/logic_monad.mli | 9 +- proofs/pfedit.ml | 22 +- proofs/pfedit.mli | 11 +- proofs/proof.ml | 21 +- proofs/proof.mli | 4 + proofs/proof_global.ml | 102 ++++-- proofs/proof_global.mli | 22 +- proofs/proof_using.ml | 172 +++++---- proofs/proof_using.mli | 15 +- proofs/proofview.ml | 51 ++- proofs/proofview.mli | 2 +- proofs/redexpr.ml | 20 +- proofs/refiner.ml | 18 +- proofs/tacmach.ml | 4 + proofs/tacmach.mli | 6 +- proofs/tactic_debug.ml | 23 +- stm/lemmas.ml | 67 ++-- stm/lemmas.mli | 3 +- stm/spawned.ml | 19 +- stm/spawned.mli | 2 +- stm/stm.ml | 191 ++++++---- stm/stm.mli | 17 +- stm/tQueue.ml | 20 + stm/tQueue.mli | 3 + stm/texmacspp.ml | 24 +- stm/vernac_classifier.ml | 24 +- stm/vio_checking.ml | 8 +- tactics/auto.ml | 54 ++- tactics/auto.mli | 9 +- tactics/autorewrite.ml | 15 +- tactics/class_tactics.ml | 67 ++-- tactics/contradiction.ml | 6 +- tactics/eauto.ml4 | 78 ++-- tactics/elim.ml | 4 +- tactics/elimschemes.ml | 26 +- tactics/eqdecide.ml | 46 ++- tactics/eqschemes.ml | 27 +- tactics/eqschemes.mli | 4 +- tactics/equality.ml | 143 ++++++-- tactics/equality.mli | 2 +- tactics/extratactics.ml4 | 27 +- tactics/hints.ml | 292 ++++++++++----- tactics/hints.mli | 39 +- tactics/hipattern.ml4 | 2 +- tactics/inv.ml | 6 +- tactics/leminv.ml | 7 +- tactics/rewrite.ml | 350 ++++++++++-------- tactics/rewrite.mli | 5 +- tactics/tacenv.ml | 46 ++- tactics/tacenv.mli | 16 + tactics/tacintern.ml | 29 +- tactics/tacinterp.ml | 53 ++- tactics/tactic_matching.mli | 4 +- tactics/tacticals.ml | 26 +- tactics/tactics.ml | 377 +++++++++++-------- tactics/tactics.mli | 1 + tactics/tauto.ml4 | 4 +- tactics/term_dnet.ml | 4 +- test-suite/Makefile | 12 +- test-suite/bugs/closed/2016.v | 62 ++++ test-suite/bugs/closed/2243.v | 9 + test-suite/bugs/closed/2584.v | 89 +++++ test-suite/bugs/closed/3267.v | 11 + test-suite/bugs/closed/3309.v | 334 ----------------- test-suite/bugs/closed/3314.v | 8 +- test-suite/bugs/closed/3330.v | 1 + test-suite/bugs/closed/3352.v | 1 + test-suite/bugs/closed/3386.v | 1 + test-suite/bugs/closed/3387.v | 1 + test-suite/bugs/closed/3446.v | 51 +++ test-suite/bugs/{opened => closed}/3461.v | 0 test-suite/bugs/closed/3509.v | 6 + test-suite/bugs/closed/3510.v | 5 + test-suite/bugs/closed/3539.v | 4 +- test-suite/bugs/closed/3559.v | 1 + test-suite/bugs/closed/3566.v | 1 + test-suite/bugs/{opened => closed}/3593.v | 2 +- test-suite/bugs/closed/3666.v | 1 + test-suite/bugs/{opened => closed}/3685.v | 2 +- test-suite/bugs/closed/3690.v | 1 + test-suite/bugs/closed/3736.v | 8 + test-suite/bugs/closed/3743.v | 11 + test-suite/bugs/closed/3777.v | 17 + test-suite/bugs/closed/3779.v | 12 + test-suite/bugs/closed/3808.v | 1 + test-suite/bugs/{opened => closed}/3819.v | 6 +- test-suite/bugs/closed/3821.v | 1 + test-suite/bugs/closed/3922.v | 3 +- test-suite/bugs/closed/3948.v | 24 ++ test-suite/bugs/closed/3956.v | 143 ++++++++ test-suite/bugs/closed/3974.v | 7 + test-suite/bugs/closed/3975.v | 8 + test-suite/bugs/closed/4034.v | 25 ++ test-suite/bugs/closed/4057.v | 210 +++++++++++ test-suite/bugs/closed/4069.v | 51 +++ test-suite/bugs/closed/4089.v | 3 +- test-suite/bugs/closed/4116.v | 383 ++++++++++++++++++++ test-suite/bugs/closed/4121.v | 1 + test-suite/bugs/closed/4151.v | 403 +++++++++++++++++++++ test-suite/bugs/closed/4161.v | 27 ++ test-suite/bugs/closed/4191.v | 5 + test-suite/bugs/closed/4198.v | 37 ++ test-suite/bugs/closed/4203.v | 19 + test-suite/bugs/closed/4205.v | 8 + test-suite/bugs/closed/4216.v | 20 + test-suite/bugs/closed/4217.v | 6 + test-suite/bugs/closed/4221.v | 9 + test-suite/bugs/closed/4232.v | 20 + test-suite/bugs/closed/4234.v | 7 + test-suite/bugs/closed/4240.v | 12 + test-suite/bugs/closed/4251.v | 17 + test-suite/bugs/closed/4254.v | 13 + test-suite/bugs/closed/4272.v | 12 + test-suite/bugs/closed/4276.v | 11 + test-suite/bugs/closed/4280.v | 24 ++ test-suite/bugs/closed/4283.v | 8 + test-suite/bugs/closed/4287.v | 125 +++++++ test-suite/bugs/closed/4294.v | 31 ++ test-suite/bugs/closed/4298.v | 7 + test-suite/bugs/closed/4299.v | 12 + test-suite/bugs/closed/4301.v | 13 + test-suite/bugs/closed/4305.v | 17 + test-suite/bugs/closed/4316.v | 3 + test-suite/bugs/closed/4318.v | 2 + test-suite/bugs/closed/4325.v | 5 + test-suite/bugs/closed/4328.v | 6 + test-suite/bugs/closed/4346.v | 2 + test-suite/bugs/closed/4347.v | 17 + test-suite/bugs/closed/4354.v | 11 + test-suite/bugs/closed/4366.v | 15 + test-suite/bugs/closed/4372.v | 20 + test-suite/bugs/closed/4375.v | 106 ++++++ test-suite/bugs/closed/4390.v | 37 ++ test-suite/bugs/closed/4394.v | 19 + test-suite/bugs/closed/4397.v | 3 + test-suite/bugs/closed/HoTT_coq_007.v | 1 + test-suite/bugs/closed/HoTT_coq_014.v | 6 +- test-suite/bugs/closed/HoTT_coq_036.v | 1 + test-suite/bugs/closed/HoTT_coq_053.v | 2 +- test-suite/bugs/closed/HoTT_coq_062.v | 1 + test-suite/bugs/closed/HoTT_coq_093.v | 3 +- test-suite/bugs/closed/HoTT_coq_108.v | 2 +- test-suite/bugs/{opened => closed}/HoTT_coq_120.v | 5 +- test-suite/bugs/opened/3045.v | 30 -- test-suite/bugs/opened/3326.v | 18 - test-suite/bugs/opened/3509.v | 19 - test-suite/bugs/opened/3510.v | 35 -- test-suite/bugs/opened/3562.v | 2 - test-suite/bugs/opened/3657.v | 33 -- test-suite/bugs/opened/3670.v | 19 - test-suite/bugs/opened/3675.v | 20 - test-suite/bugs/opened/3754.v | 1 + test-suite/bugs/opened/3788.v | 5 - test-suite/bugs/opened/3808.v | 2 - test-suite/bugs/opened/4214.v | 5 + test-suite/coqchk/primproj.v | 2 + test-suite/failure/guard-cofix.v | 2 +- test-suite/ide/bug4246.fake | 14 + test-suite/ide/bug4249.fake | 16 + test-suite/ide/reopen.fake | 21 ++ test-suite/ide/univ.fake | 14 + test-suite/interactive/4289.v | 14 + test-suite/interactive/ParalITP_smallproofs.v | 0 test-suite/kernel/vm-univ.v | 145 ++++++++ test-suite/output/Inductive.out | 3 + test-suite/output/Inductive.v | 3 + test-suite/output/Notations.out | 4 +- test-suite/output/PrintAssumptions.out | 7 +- test-suite/output/PrintAssumptions.v | 16 + test-suite/output/PrintModule.out | 4 + test-suite/output/PrintModule.v | 34 ++ test-suite/output/inference.out | 4 +- test-suite/output/ltac.out | 2 + test-suite/output/ltac.v | 17 + test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v | 0 test-suite/success/Hints.v | 44 +++ test-suite/success/apply.v | 47 ++- test-suite/success/auto.v | 2 +- test-suite/success/extraction_polyprop.v | 11 + test-suite/success/intros.v | 36 ++ test-suite/success/ltac.v | 19 + test-suite/success/namedunivs.v | 2 + test-suite/success/polymorphism.v | 30 ++ test-suite/success/primitiveproj.v | 7 + test-suite/success/proof_using.v | 76 ++++ test-suite/success/record_syntax.v | 47 +++ test-suite/success/sideff.v | 12 + test-suite/success/simpl.v | 7 + test-suite/success/specialize.v | 20 +- test-suite/success/univnames.v | 26 ++ theories/Arith/intro.tex | 55 --- theories/Bool/intro.tex | 16 - theories/Classes/CMorphisms.v | 8 +- theories/Classes/RelationClasses.v | 5 + theories/Compat/Coq84.v | 77 ++++ pretyping/vnorm.mli => theories/Compat/Coq85.v | 7 +- theories/Compat/vo.itarget | 2 + theories/Lists/List.v | 20 +- theories/Lists/intro.tex | 20 - theories/Logic/WeakFan.v | 11 +- theories/Logic/intro.tex | 8 - theories/NArith/intro.tex | 5 - theories/Numbers/Cyclic/Int31/Int31.v | 2 +- theories/Numbers/NaryFunctions.v | 2 +- theories/PArith/intro.tex | 4 - theories/Program/Syntax.v | 7 - theories/Program/Tactics.v | 2 +- theories/Reals/intro.tex | 4 - theories/Relations/intro.tex | 23 -- theories/Setoids/intro.tex | 1 - theories/Sets/intro.tex | 24 -- theories/Sorting/intro.tex | 1 - theories/Vectors/Fin.v | 32 +- theories/Vectors/VectorSpec.v | 45 ++- theories/Wellfounded/intro.tex | 4 - theories/ZArith/intro.tex | 6 - theories/theories.itarget | 1 + tools/README.coq-tex | 13 - tools/README.emacs | 0 tools/coq-sl.sty | 0 tools/coq_makefile.ml | 23 +- tools/coq_tex.ml | 203 +++++------ tools/coqc.ml | 15 +- tools/coqdep.ml | 64 ++-- tools/coqdep_boot.ml | 6 +- tools/coqdep_common.ml | 155 +++++--- tools/coqdep_common.mli | 10 +- tools/coqdep_lexer.mli | 3 +- tools/coqdep_lexer.mll | 16 +- tools/coqdoc/cpretty.mll | 1 + tools/coqdoc/main.ml | 8 +- tools/coqdoc/output.ml | 7 +- tools/coqwc.mll | 4 +- tools/fake_ide.ml | 6 +- tools/gallina.ml | 5 +- {library => toplevel}/assumptions.ml | 107 +++--- {library => toplevel}/assumptions.mli | 23 +- toplevel/auto_ind_decl.ml | 123 ++++--- toplevel/auto_ind_decl.mli | 1 + toplevel/cerrors.ml | 17 +- toplevel/cerrors.mli | 2 +- toplevel/class.ml | 13 +- toplevel/classes.ml | 23 +- toplevel/command.ml | 328 ++++++++++------- toplevel/command.mli | 40 +- toplevel/coqinit.ml | 5 +- toplevel/coqloop.ml | 2 +- toplevel/coqtop.ml | 125 ++++--- toplevel/coqtop.mli | 2 +- toplevel/discharge.ml | 4 +- toplevel/himsg.ml | 22 +- toplevel/ind_tables.ml | 60 +-- toplevel/ind_tables.mli | 19 +- toplevel/indschemes.ml | 52 +-- toplevel/locality.ml | 5 +- toplevel/metasyntax.ml | 41 ++- toplevel/metasyntax.mli | 1 + toplevel/mltop.ml | 13 +- toplevel/obligations.ml | 221 +++++------ toplevel/obligations.mli | 4 +- toplevel/record.ml | 122 ++++--- toplevel/record.mli | 2 +- toplevel/search.ml | 8 +- toplevel/toplevel.mllib | 1 + toplevel/usage.ml | 21 +- toplevel/vernac.ml | 77 ++-- toplevel/vernacentries.ml | 287 ++++++++------- toplevel/vernacentries.mli | 3 + 564 files changed, 12811 insertions(+), 7066 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