[Pkg-ocaml-maint-commits] [coq] 03/05: Imported Upstream version 8.5~beta3+dfsg
Enrico Tassi
gareuselesinge at moszumanska.debian.org
Sat Nov 14 09:20:24 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 4e76c4f01b69b77f40686e06c4544aa156efaa5a
Merge: 64fa31c 91dbeab
Author: Enrico Tassi <gareuselesinge at 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
More information about the Pkg-ocaml-maint-commits
mailing list