From 3e0334dd48b5d0b03046d0aff1a82867dc98d656 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 14:19:44 +0200 Subject: Bump year in headers. --- API/API.ml | 2 +- API/API.mli | 2 +- API/grammar_API.ml | 2 +- API/grammar_API.mli | 2 +- checker/check.ml | 2 +- checker/check_stat.ml | 2 +- checker/check_stat.mli | 2 +- checker/checker.ml | 2 +- checker/cic.mli | 2 +- checker/closure.ml | 2 +- checker/closure.mli | 2 +- checker/indtypes.ml | 2 +- checker/indtypes.mli | 2 +- checker/inductive.ml | 2 +- checker/inductive.mli | 2 +- checker/mod_checking.mli | 2 +- checker/modops.ml | 2 +- checker/modops.mli | 2 +- checker/print.ml | 2 +- checker/reduction.ml | 2 +- checker/reduction.mli | 2 +- checker/safe_typing.ml | 2 +- checker/safe_typing.mli | 2 +- checker/subtyping.ml | 2 +- checker/subtyping.mli | 2 +- checker/term.ml | 2 +- checker/type_errors.ml | 2 +- checker/type_errors.mli | 2 +- checker/typeops.ml | 2 +- checker/typeops.mli | 2 +- checker/univ.ml | 2 +- checker/univ.mli | 2 +- checker/validate.ml | 2 +- checker/values.ml | 4 ++-- checker/votour.ml | 2 +- config/coq_config.mli | 2 +- dev/db_printers.ml | 2 +- dev/header | 2 +- dev/top_printers.ml | 2 +- engine/eConstr.ml | 2 +- engine/eConstr.mli | 2 +- engine/evarutil.ml | 2 +- engine/evarutil.mli | 2 +- engine/evd.ml | 2 +- engine/evd.mli | 2 +- engine/ftactic.ml | 2 +- engine/ftactic.mli | 2 +- engine/geninterp.ml | 2 +- engine/geninterp.mli | 2 +- engine/logic_monad.ml | 2 +- engine/logic_monad.mli | 2 +- engine/namegen.ml | 2 +- engine/namegen.mli | 2 +- engine/proofview.ml | 2 +- engine/proofview.mli | 2 +- engine/proofview_monad.ml | 2 +- engine/proofview_monad.mli | 2 +- engine/termops.ml | 2 +- engine/termops.mli | 2 +- engine/universes.ml | 2 +- engine/universes.mli | 2 +- grammar/argextend.mlp | 2 +- grammar/compat5.ml | 2 +- grammar/q_util.mli | 2 +- grammar/q_util.mlp | 2 +- grammar/tacextend.mlp | 2 +- grammar/vernacextend.mlp | 2 +- ide/config_lexer.mll | 2 +- ide/coq.ml | 2 +- ide/coq.mli | 2 +- ide/coqOps.ml | 2 +- ide/coqOps.mli | 2 +- ide/coq_commands.ml | 2 +- ide/coq_lex.mll | 2 +- ide/coqide.ml | 2 +- ide/coqide.mli | 2 +- ide/coqide_main.ml4 | 2 +- ide/fileOps.ml | 2 +- ide/fileOps.mli | 2 +- ide/gtk_parsing.ml | 2 +- ide/ide_slave.ml | 2 +- ide/ideutils.ml | 2 +- ide/ideutils.mli | 2 +- ide/interface.mli | 2 +- ide/nanoPG.ml | 2 +- ide/preferences.ml | 2 +- ide/preferences.mli | 2 +- ide/richpp.ml | 2 +- ide/richpp.mli | 2 +- ide/sentence.ml | 2 +- ide/sentence.mli | 2 +- ide/serialize.ml | 2 +- ide/serialize.mli | 2 +- ide/session.ml | 2 +- ide/session.mli | 2 +- ide/tags.ml | 2 +- ide/tags.mli | 2 +- ide/utf8_convert.mll | 2 +- ide/wg_Command.ml | 2 +- ide/wg_Command.mli | 2 +- ide/wg_Completion.ml | 2 +- ide/wg_Completion.mli | 2 +- ide/wg_Detachable.ml | 2 +- ide/wg_Detachable.mli | 2 +- ide/wg_Find.ml | 2 +- ide/wg_Find.mli | 2 +- ide/wg_MessageView.ml | 2 +- ide/wg_MessageView.mli | 2 +- ide/wg_Notebook.ml | 2 +- ide/wg_Notebook.mli | 2 +- ide/wg_ProofView.ml | 2 +- ide/wg_ProofView.mli | 2 +- ide/wg_ScriptView.ml | 2 +- ide/wg_ScriptView.mli | 2 +- ide/wg_Segment.ml | 2 +- ide/wg_Segment.mli | 2 +- ide/xml_printer.ml | 2 +- ide/xml_printer.mli | 2 +- ide/xmlprotocol.ml | 2 +- ide/xmlprotocol.mli | 2 +- interp/constrexpr_ops.ml | 2 +- interp/constrexpr_ops.mli | 2 +- interp/constrextern.ml | 2 +- interp/constrextern.mli | 2 +- interp/constrintern.ml | 2 +- interp/constrintern.mli | 2 +- interp/dumpglob.ml | 2 +- interp/dumpglob.mli | 2 +- interp/genintern.ml | 2 +- interp/genintern.mli | 2 +- interp/implicit_quantifiers.ml | 2 +- interp/implicit_quantifiers.mli | 2 +- interp/modintern.ml | 2 +- interp/modintern.mli | 2 +- interp/notation.ml | 2 +- interp/notation.mli | 2 +- interp/notation_ops.ml | 2 +- interp/notation_ops.mli | 2 +- interp/ppextend.ml | 2 +- interp/ppextend.mli | 2 +- interp/reserve.ml | 2 +- interp/reserve.mli | 2 +- interp/smartlocate.ml | 2 +- interp/smartlocate.mli | 2 +- interp/stdarg.ml | 2 +- interp/stdarg.mli | 2 +- interp/syntax_def.ml | 2 +- interp/syntax_def.mli | 2 +- interp/topconstr.ml | 2 +- interp/topconstr.mli | 2 +- intf/constrexpr.ml | 2 +- intf/decl_kinds.ml | 2 +- intf/evar_kinds.ml | 2 +- intf/extend.ml | 2 +- intf/genredexpr.ml | 2 +- intf/glob_term.ml | 2 +- intf/locus.ml | 2 +- intf/misctypes.ml | 2 +- intf/notation_term.ml | 2 +- intf/pattern.ml | 2 +- intf/tactypes.ml | 2 +- intf/vernacexpr.ml | 2 +- kernel/cClosure.ml | 2 +- kernel/cClosure.mli | 2 +- kernel/cbytecodes.ml | 2 +- kernel/cbytecodes.mli | 2 +- kernel/cbytegen.ml | 2 +- kernel/cemitcodes.ml | 2 +- kernel/constr.ml | 2 +- kernel/constr.mli | 2 +- kernel/context.ml | 2 +- kernel/context.mli | 2 +- kernel/conv_oracle.ml | 2 +- kernel/conv_oracle.mli | 2 +- kernel/cooking.ml | 2 +- kernel/cooking.mli | 2 +- kernel/csymtable.ml | 2 +- kernel/csymtable.mli | 2 +- kernel/declarations.ml | 2 +- kernel/declareops.ml | 2 +- kernel/declareops.mli | 2 +- kernel/entries.mli | 2 +- kernel/environ.ml | 2 +- kernel/environ.mli | 2 +- kernel/esubst.ml | 2 +- kernel/esubst.mli | 2 +- kernel/evar.ml | 2 +- kernel/evar.mli | 2 +- kernel/indtypes.ml | 2 +- kernel/indtypes.mli | 2 +- kernel/inductive.ml | 2 +- kernel/inductive.mli | 2 +- kernel/mod_subst.ml | 2 +- kernel/mod_subst.mli | 2 +- kernel/mod_typing.ml | 2 +- kernel/mod_typing.mli | 2 +- kernel/modops.ml | 2 +- kernel/modops.mli | 2 +- kernel/names.ml | 2 +- kernel/names.mli | 2 +- kernel/nativecode.ml | 2 +- kernel/nativecode.mli | 2 +- kernel/nativeconv.ml | 2 +- kernel/nativeconv.mli | 2 +- kernel/nativeinstr.mli | 2 +- kernel/nativelambda.ml | 2 +- kernel/nativelambda.mli | 2 +- kernel/nativelib.ml | 2 +- kernel/nativelib.mli | 2 +- kernel/nativelibrary.ml | 2 +- kernel/nativelibrary.mli | 2 +- kernel/nativevalues.ml | 2 +- kernel/nativevalues.mli | 2 +- kernel/opaqueproof.ml | 2 +- kernel/opaqueproof.mli | 2 +- kernel/pre_env.ml | 2 +- kernel/pre_env.mli | 2 +- kernel/primitives.ml | 2 +- kernel/primitives.mli | 2 +- kernel/reduction.ml | 2 +- kernel/reduction.mli | 2 +- kernel/retroknowledge.ml | 2 +- kernel/retroknowledge.mli | 2 +- kernel/safe_typing.ml | 2 +- kernel/safe_typing.mli | 2 +- kernel/sorts.ml | 2 +- kernel/sorts.mli | 2 +- kernel/subtyping.ml | 2 +- kernel/subtyping.mli | 2 +- kernel/term.ml | 2 +- kernel/term.mli | 2 +- kernel/term_typing.ml | 2 +- kernel/term_typing.mli | 2 +- kernel/type_errors.ml | 2 +- kernel/type_errors.mli | 2 +- kernel/typeops.ml | 2 +- kernel/typeops.mli | 2 +- kernel/univ.ml | 2 +- kernel/univ.mli | 2 +- kernel/vars.ml | 2 +- kernel/vars.mli | 2 +- kernel/vconv.mli | 2 +- kernel/vm.ml | 2 +- lib/aux_file.ml | 2 +- lib/aux_file.mli | 2 +- lib/bigint.ml | 2 +- lib/bigint.mli | 2 +- lib/cEphemeron.ml | 2 +- lib/cEphemeron.mli | 2 +- lib/cMap.ml | 2 +- lib/cMap.mli | 2 +- lib/cSet.ml | 2 +- lib/cSet.mli | 2 +- lib/cString.ml | 2 +- lib/cString.mli | 2 +- lib/cThread.ml | 2 +- lib/cThread.mli | 2 +- lib/cUnix.ml | 2 +- lib/cUnix.mli | 2 +- lib/cWarnings.ml | 2 +- lib/cWarnings.mli | 2 +- lib/canary.ml | 2 +- lib/canary.mli | 2 +- lib/control.ml | 2 +- lib/control.mli | 2 +- lib/coqProject_file.ml4 | 2 +- lib/coqProject_file.mli | 2 +- lib/deque.ml | 2 +- lib/deque.mli | 2 +- lib/dyn.ml | 2 +- lib/dyn.mli | 2 +- lib/envars.ml | 2 +- lib/envars.mli | 2 +- lib/explore.ml | 2 +- lib/explore.mli | 2 +- lib/feedback.ml | 2 +- lib/feedback.mli | 2 +- lib/flags.ml | 2 +- lib/flags.mli | 2 +- lib/future.ml | 2 +- lib/future.mli | 2 +- lib/genarg.ml | 2 +- lib/genarg.mli | 2 +- lib/hMap.ml | 2 +- lib/hMap.mli | 2 +- lib/hashcons.ml | 2 +- lib/hashcons.mli | 2 +- lib/hashset.ml | 2 +- lib/hashset.mli | 2 +- lib/heap.ml | 2 +- lib/heap.mli | 2 +- lib/hook.ml | 2 +- lib/hook.mli | 2 +- lib/iStream.ml | 2 +- lib/iStream.mli | 2 +- lib/int.ml | 2 +- lib/int.mli | 2 +- lib/loc.ml | 2 +- lib/loc.mli | 2 +- lib/minisys.ml | 2 +- lib/option.ml | 2 +- lib/option.mli | 2 +- lib/pp.ml | 2 +- lib/pp.mli | 2 +- lib/profile.ml | 2 +- lib/profile.mli | 2 +- lib/remoteCounter.ml | 2 +- lib/remoteCounter.mli | 2 +- lib/rtree.ml | 2 +- lib/rtree.mli | 2 +- lib/spawn.ml | 2 +- lib/spawn.mli | 2 +- lib/system.ml | 2 +- lib/system.mli | 2 +- lib/terminal.ml | 2 +- lib/terminal.mli | 2 +- lib/trie.ml | 2 +- lib/trie.mli | 2 +- lib/unicode.mli | 2 +- lib/unionfind.ml | 2 +- lib/unionfind.mli | 2 +- lib/util.mli | 2 +- lib/xml_datatype.mli | 2 +- library/coqlib.ml | 2 +- library/coqlib.mli | 2 +- library/declare.ml | 2 +- library/declare.mli | 2 +- library/declaremods.ml | 2 +- library/declaremods.mli | 2 +- library/decls.ml | 2 +- library/decls.mli | 2 +- library/dischargedhypsmap.ml | 2 +- library/dischargedhypsmap.mli | 2 +- library/global.ml | 2 +- library/global.mli | 2 +- library/globnames.ml | 2 +- library/globnames.mli | 2 +- library/goptions.ml | 2 +- library/goptions.mli | 2 +- library/heads.ml | 2 +- library/heads.mli | 2 +- library/impargs.ml | 2 +- library/impargs.mli | 2 +- library/keys.ml | 2 +- library/keys.mli | 2 +- library/kindops.ml | 2 +- library/kindops.mli | 2 +- library/lib.ml | 2 +- library/lib.mli | 2 +- library/libnames.ml | 2 +- library/libnames.mli | 2 +- library/libobject.ml | 2 +- library/libobject.mli | 2 +- library/library.ml | 2 +- library/library.mli | 2 +- library/loadpath.ml | 2 +- library/loadpath.mli | 2 +- library/nameops.ml | 2 +- library/nameops.mli | 2 +- library/nametab.ml | 2 +- library/nametab.mli | 2 +- library/states.ml | 2 +- library/states.mli | 2 +- library/summary.ml | 2 +- library/summary.mli | 2 +- library/univops.ml | 2 +- library/univops.mli | 2 +- parsing/cLexer.ml4 | 2 +- parsing/cLexer.mli | 2 +- parsing/egramcoq.ml | 2 +- parsing/egramcoq.mli | 2 +- parsing/egramml.ml | 2 +- parsing/egramml.mli | 2 +- parsing/g_constr.ml4 | 2 +- parsing/g_prim.ml4 | 2 +- parsing/g_proofs.ml4 | 2 +- parsing/g_vernac.ml4 | 2 +- parsing/pcoq.ml | 2 +- parsing/pcoq.mli | 2 +- parsing/tok.ml | 2 +- parsing/tok.mli | 2 +- plugins/btauto/g_btauto.ml4 | 2 +- plugins/cc/ccalgo.ml | 2 +- plugins/cc/ccalgo.mli | 2 +- plugins/cc/ccproof.ml | 2 +- plugins/cc/ccproof.mli | 2 +- plugins/cc/cctac.ml | 2 +- plugins/cc/g_congruence.ml4 | 2 +- plugins/derive/derive.ml | 2 +- plugins/derive/derive.mli | 2 +- plugins/derive/g_derive.ml4 | 2 +- plugins/extraction/ExtrOcamlBasic.v | 2 +- plugins/extraction/ExtrOcamlBigIntConv.v | 2 +- plugins/extraction/ExtrOcamlIntConv.v | 2 +- plugins/extraction/ExtrOcamlNatBigInt.v | 2 +- plugins/extraction/ExtrOcamlNatInt.v | 2 +- plugins/extraction/ExtrOcamlString.v | 2 +- plugins/extraction/ExtrOcamlZBigInt.v | 2 +- plugins/extraction/ExtrOcamlZInt.v | 2 +- plugins/extraction/Extraction.v | 2 +- plugins/extraction/big.ml | 2 +- plugins/extraction/common.ml | 2 +- plugins/extraction/common.mli | 2 +- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/extraction.ml | 2 +- plugins/extraction/extraction.mli | 2 +- plugins/extraction/g_extraction.ml4 | 2 +- plugins/extraction/haskell.ml | 2 +- plugins/extraction/haskell.mli | 2 +- plugins/extraction/miniml.mli | 2 +- plugins/extraction/mlutil.ml | 2 +- plugins/extraction/mlutil.mli | 2 +- plugins/extraction/modutil.ml | 2 +- plugins/extraction/modutil.mli | 2 +- plugins/extraction/ocaml.ml | 2 +- plugins/extraction/ocaml.mli | 2 +- plugins/extraction/scheme.ml | 2 +- plugins/extraction/scheme.mli | 2 +- plugins/extraction/table.ml | 2 +- plugins/extraction/table.mli | 2 +- plugins/firstorder/formula.ml | 2 +- plugins/firstorder/formula.mli | 2 +- plugins/firstorder/g_ground.ml4 | 2 +- plugins/firstorder/ground.ml | 2 +- plugins/firstorder/ground.mli | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/firstorder/instances.mli | 2 +- plugins/firstorder/rules.ml | 2 +- plugins/firstorder/rules.mli | 2 +- plugins/firstorder/sequent.ml | 2 +- plugins/firstorder/sequent.mli | 2 +- plugins/firstorder/unify.ml | 2 +- plugins/firstorder/unify.mli | 2 +- plugins/fourier/Fourier.v | 2 +- plugins/fourier/Fourier_util.v | 2 +- plugins/fourier/fourier.ml | 2 +- plugins/fourier/fourierR.ml | 2 +- plugins/fourier/g_fourier.ml4 | 2 +- plugins/funind/FunInd.v | 2 +- plugins/funind/Recdef.v | 2 +- plugins/funind/functional_principles_types.mli | 2 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/merge.ml | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ltac/coretactics.ml4 | 2 +- plugins/ltac/evar_tactics.ml | 2 +- plugins/ltac/evar_tactics.mli | 2 +- plugins/ltac/extraargs.ml4 | 2 +- plugins/ltac/extraargs.mli | 2 +- plugins/ltac/extratactics.ml4 | 2 +- plugins/ltac/extratactics.mli | 2 +- plugins/ltac/g_class.ml4 | 2 +- plugins/ltac/g_eqdecide.ml4 | 2 +- plugins/ltac/g_ltac.ml4 | 2 +- plugins/ltac/g_obligations.ml4 | 2 +- plugins/ltac/g_rewrite.ml4 | 2 +- plugins/ltac/g_tactic.ml4 | 2 +- plugins/ltac/pltac.ml | 2 +- plugins/ltac/pltac.mli | 2 +- plugins/ltac/pptactic.ml | 2 +- plugins/ltac/pptactic.mli | 2 +- plugins/ltac/profile_ltac.ml | 2 +- plugins/ltac/profile_ltac.mli | 2 +- plugins/ltac/profile_ltac_tactics.ml4 | 2 +- plugins/ltac/rewrite.ml | 2 +- plugins/ltac/rewrite.mli | 2 +- plugins/ltac/tacarg.ml | 2 +- plugins/ltac/tacarg.mli | 2 +- plugins/ltac/taccoerce.ml | 2 +- plugins/ltac/taccoerce.mli | 2 +- plugins/ltac/tacentries.ml | 2 +- plugins/ltac/tacentries.mli | 2 +- plugins/ltac/tacenv.ml | 2 +- plugins/ltac/tacenv.mli | 2 +- plugins/ltac/tacexpr.mli | 2 +- plugins/ltac/tacintern.ml | 2 +- plugins/ltac/tacintern.mli | 2 +- plugins/ltac/tacinterp.ml | 2 +- plugins/ltac/tacinterp.mli | 2 +- plugins/ltac/tacsubst.ml | 2 +- plugins/ltac/tacsubst.mli | 2 +- plugins/ltac/tactic_debug.ml | 2 +- plugins/ltac/tactic_debug.mli | 2 +- plugins/ltac/tactic_matching.ml | 2 +- plugins/ltac/tactic_option.ml | 2 +- plugins/ltac/tactic_option.mli | 2 +- plugins/ltac/tauto.ml | 2 +- plugins/micromega/Env.v | 2 +- plugins/micromega/EnvRing.v | 2 +- plugins/micromega/Lia.v | 2 +- plugins/micromega/Lqa.v | 2 +- plugins/micromega/Lra.v | 2 +- plugins/micromega/MExtraction.v | 2 +- plugins/micromega/OrderedRing.v | 2 +- plugins/micromega/Psatz.v | 2 +- plugins/micromega/QMicromega.v | 2 +- plugins/micromega/RMicromega.v | 2 +- plugins/micromega/Refl.v | 2 +- plugins/micromega/RingMicromega.v | 2 +- plugins/micromega/Tauto.v | 2 +- plugins/micromega/ZCoeff.v | 2 +- plugins/micromega/ZMicromega.v | 2 +- plugins/micromega/certificate.ml | 2 +- plugins/micromega/coq_micromega.ml | 2 +- plugins/micromega/csdpcert.ml | 2 +- plugins/micromega/g_micromega.ml4 | 2 +- plugins/micromega/mutils.ml | 2 +- plugins/micromega/persistent_cache.ml | 2 +- plugins/micromega/polynomial.ml | 2 +- plugins/micromega/sos.mli | 2 +- plugins/micromega/sos_types.ml | 2 +- plugins/micromega/sos_types.mli | 2 +- plugins/nsatz/Nsatz.v | 2 +- plugins/nsatz/g_nsatz.ml4 | 2 +- plugins/nsatz/ideal.ml | 2 +- plugins/nsatz/ideal.mli | 2 +- plugins/nsatz/nsatz.ml | 2 +- plugins/nsatz/nsatz.mli | 2 +- plugins/nsatz/polynom.ml | 2 +- plugins/nsatz/polynom.mli | 2 +- plugins/omega/Omega.v | 2 +- plugins/omega/OmegaPlugin.v | 2 +- plugins/omega/OmegaTactic.v | 2 +- plugins/omega/PreOmega.v | 2 +- plugins/omega/coq_omega.ml | 2 +- plugins/omega/g_omega.ml4 | 2 +- plugins/omega/omega.ml | 2 +- plugins/quote/Quote.v | 2 +- plugins/quote/g_quote.ml4 | 2 +- plugins/quote/quote.ml | 2 +- plugins/rtauto/Bintree.v | 2 +- plugins/rtauto/Rtauto.v | 2 +- plugins/rtauto/g_rtauto.ml4 | 2 +- plugins/rtauto/proof_search.ml | 2 +- plugins/rtauto/proof_search.mli | 2 +- plugins/rtauto/refl_tauto.ml | 2 +- plugins/rtauto/refl_tauto.mli | 2 +- plugins/setoid_ring/ArithRing.v | 2 +- plugins/setoid_ring/BinList.v | 2 +- plugins/setoid_ring/Cring.v | 2 +- plugins/setoid_ring/Field.v | 2 +- plugins/setoid_ring/Field_tac.v | 2 +- plugins/setoid_ring/Field_theory.v | 2 +- plugins/setoid_ring/InitialRing.v | 2 +- plugins/setoid_ring/NArithRing.v | 2 +- plugins/setoid_ring/Ncring.v | 2 +- plugins/setoid_ring/Ncring_initial.v | 2 +- plugins/setoid_ring/Ncring_polynom.v | 2 +- plugins/setoid_ring/Ncring_tac.v | 2 +- plugins/setoid_ring/Ring.v | 2 +- plugins/setoid_ring/Ring_base.v | 2 +- plugins/setoid_ring/Ring_polynom.v | 2 +- plugins/setoid_ring/Ring_theory.v | 2 +- plugins/setoid_ring/ZArithRing.v | 2 +- plugins/setoid_ring/newring.ml | 2 +- plugins/ssrmatching/ssrmatching.ml4 | 2 +- plugins/syntax/int31_syntax.ml | 2 +- plugins/syntax/nat_syntax.ml | 2 +- plugins/syntax/r_syntax.ml | 2 +- plugins/syntax/z_syntax.ml | 2 +- pretyping/arguments_renaming.ml | 2 +- pretyping/arguments_renaming.mli | 2 +- pretyping/cases.ml | 2 +- pretyping/cases.mli | 2 +- pretyping/cbv.ml | 2 +- pretyping/cbv.mli | 2 +- pretyping/classops.ml | 2 +- pretyping/classops.mli | 2 +- pretyping/coercion.ml | 2 +- pretyping/coercion.mli | 2 +- pretyping/constr_matching.ml | 2 +- pretyping/constr_matching.mli | 2 +- pretyping/detyping.ml | 2 +- pretyping/detyping.mli | 2 +- pretyping/evarconv.ml | 2 +- pretyping/evarconv.mli | 2 +- pretyping/evardefine.ml | 2 +- pretyping/evardefine.mli | 2 +- pretyping/evarsolve.ml | 2 +- pretyping/evarsolve.mli | 2 +- pretyping/find_subterm.ml | 2 +- pretyping/find_subterm.mli | 2 +- pretyping/glob_ops.ml | 2 +- pretyping/glob_ops.mli | 2 +- pretyping/indrec.ml | 2 +- pretyping/indrec.mli | 2 +- pretyping/inductiveops.ml | 2 +- pretyping/inductiveops.mli | 2 +- pretyping/locusops.ml | 2 +- pretyping/locusops.mli | 2 +- pretyping/miscops.ml | 2 +- pretyping/miscops.mli | 2 +- pretyping/nativenorm.ml | 2 +- pretyping/nativenorm.mli | 2 +- pretyping/patternops.ml | 2 +- pretyping/patternops.mli | 2 +- pretyping/pretype_errors.ml | 2 +- pretyping/pretype_errors.mli | 2 +- pretyping/pretyping.ml | 2 +- pretyping/pretyping.mli | 2 +- pretyping/program.ml | 2 +- pretyping/program.mli | 2 +- pretyping/recordops.ml | 2 +- pretyping/recordops.mli | 2 +- pretyping/redops.ml | 2 +- pretyping/redops.mli | 2 +- pretyping/reductionops.ml | 2 +- pretyping/reductionops.mli | 2 +- pretyping/retyping.ml | 2 +- pretyping/retyping.mli | 2 +- pretyping/tacred.ml | 2 +- pretyping/tacred.mli | 2 +- pretyping/typeclasses.ml | 2 +- pretyping/typeclasses.mli | 2 +- pretyping/typeclasses_errors.ml | 2 +- pretyping/typeclasses_errors.mli | 2 +- pretyping/typing.ml | 2 +- pretyping/typing.mli | 2 +- pretyping/unification.ml | 2 +- pretyping/unification.mli | 2 +- pretyping/vnorm.ml | 2 +- pretyping/vnorm.mli | 2 +- printing/genprint.ml | 2 +- printing/genprint.mli | 2 +- printing/miscprint.ml | 2 +- printing/miscprint.mli | 2 +- printing/ppconstr.ml | 2 +- printing/ppconstr.mli | 2 +- printing/pputils.ml | 2 +- printing/pputils.mli | 2 +- printing/ppvernac.ml | 2 +- printing/ppvernac.mli | 2 +- printing/prettyp.ml | 2 +- printing/prettyp.mli | 2 +- printing/printer.ml | 2 +- printing/printer.mli | 2 +- printing/printmod.ml | 2 +- printing/printmod.mli | 2 +- proofs/clenv.ml | 2 +- proofs/clenv.mli | 2 +- proofs/clenvtac.ml | 2 +- proofs/clenvtac.mli | 2 +- proofs/evar_refiner.ml | 2 +- proofs/evar_refiner.mli | 2 +- proofs/goal.ml | 2 +- proofs/goal.mli | 2 +- proofs/logic.ml | 2 +- proofs/logic.mli | 2 +- proofs/pfedit.ml | 2 +- proofs/pfedit.mli | 2 +- proofs/proof.ml | 2 +- proofs/proof.mli | 2 +- proofs/proof_global.ml | 2 +- proofs/proof_global.mli | 2 +- proofs/proof_type.mli | 2 +- proofs/proof_using.ml | 2 +- proofs/proof_using.mli | 2 +- proofs/redexpr.ml | 2 +- proofs/redexpr.mli | 2 +- proofs/refine.ml | 2 +- proofs/refine.mli | 2 +- proofs/refiner.ml | 2 +- proofs/refiner.mli | 2 +- proofs/tacmach.ml | 2 +- proofs/tacmach.mli | 2 +- stm/asyncTaskQueue.ml | 2 +- stm/asyncTaskQueue.mli | 2 +- stm/coqworkmgrApi.ml | 2 +- stm/coqworkmgrApi.mli | 2 +- stm/dag.ml | 2 +- stm/dag.mli | 2 +- stm/proofBlockDelimiter.ml | 2 +- stm/proofBlockDelimiter.mli | 2 +- stm/proofworkertop.ml | 2 +- stm/queryworkertop.ml | 2 +- stm/spawned.ml | 2 +- stm/spawned.mli | 2 +- stm/stm.ml | 2 +- stm/tQueue.ml | 2 +- stm/tQueue.mli | 2 +- stm/tacworkertop.ml | 2 +- stm/vcs.ml | 2 +- stm/vcs.mli | 2 +- stm/vernac_classifier.ml | 2 +- stm/vernac_classifier.mli | 2 +- stm/vio_checking.ml | 2 +- stm/vio_checking.mli | 2 +- stm/workerLoop.ml | 2 +- stm/workerLoop.mli | 2 +- stm/workerPool.ml | 2 +- stm/workerPool.mli | 2 +- tactics/auto.ml | 2 +- tactics/auto.mli | 2 +- tactics/autorewrite.ml | 2 +- tactics/autorewrite.mli | 2 +- tactics/btermdn.ml | 2 +- tactics/btermdn.mli | 2 +- tactics/class_tactics.ml | 2 +- tactics/class_tactics.mli | 2 +- tactics/contradiction.ml | 2 +- tactics/contradiction.mli | 2 +- tactics/dnet.ml | 2 +- tactics/dnet.mli | 2 +- tactics/eauto.ml | 2 +- tactics/eauto.mli | 2 +- tactics/elim.ml | 2 +- tactics/elim.mli | 2 +- tactics/elimschemes.ml | 2 +- tactics/elimschemes.mli | 2 +- tactics/eqdecide.ml | 2 +- tactics/eqdecide.mli | 2 +- tactics/eqschemes.ml | 2 +- tactics/eqschemes.mli | 2 +- tactics/equality.ml | 2 +- tactics/equality.mli | 2 +- tactics/hints.ml | 2 +- tactics/hints.mli | 2 +- tactics/hipattern.ml | 2 +- tactics/hipattern.mli | 2 +- tactics/inv.ml | 2 +- tactics/inv.mli | 2 +- tactics/leminv.ml | 2 +- tactics/leminv.mli | 2 +- tactics/tacticals.ml | 2 +- tactics/tacticals.mli | 2 +- tactics/tactics.ml | 2 +- tactics/tactics.mli | 2 +- tactics/term_dnet.ml | 2 +- tactics/term_dnet.mli | 2 +- test-suite/failure/Tauto.v | 2 +- test-suite/failure/clash_cons.v | 2 +- test-suite/failure/fixpoint1.v | 2 +- test-suite/failure/guard.v | 2 +- test-suite/failure/illtype1.v | 2 +- test-suite/failure/positivity.v | 2 +- test-suite/failure/redef.v | 2 +- test-suite/failure/search.v | 2 +- test-suite/ideal-features/Apply.v | 2 +- test-suite/success/Check.v | 2 +- test-suite/success/Field.v | 2 +- test-suite/success/Tauto.v | 2 +- test-suite/success/TestRefine.v | 2 +- test-suite/success/eauto.v | 2 +- test-suite/success/eqdecide.v | 2 +- test-suite/success/extraction.v | 2 +- test-suite/success/inds_type_sec.v | 2 +- test-suite/success/induct.v | 2 +- test-suite/success/mutual_ind.v | 2 +- test-suite/success/unfold.v | 2 +- test-suite/typeclasses/NewSetoid.v | 2 +- theories/Arith/Arith.v | 2 +- theories/Arith/Arith_base.v | 2 +- theories/Arith/Between.v | 2 +- theories/Arith/Bool_nat.v | 2 +- theories/Arith/Compare.v | 2 +- theories/Arith/Compare_dec.v | 2 +- theories/Arith/Div2.v | 2 +- theories/Arith/EqNat.v | 2 +- theories/Arith/Euclid.v | 2 +- theories/Arith/Even.v | 2 +- theories/Arith/Factorial.v | 2 +- theories/Arith/Gt.v | 2 +- theories/Arith/Le.v | 2 +- theories/Arith/Lt.v | 2 +- theories/Arith/Max.v | 2 +- theories/Arith/Min.v | 2 +- theories/Arith/Minus.v | 2 +- theories/Arith/Mult.v | 2 +- theories/Arith/PeanoNat.v | 2 +- theories/Arith/Peano_dec.v | 2 +- theories/Arith/Wf_nat.v | 2 +- theories/Bool/Bool.v | 2 +- theories/Bool/BoolEq.v | 2 +- theories/Bool/Bvector.v | 2 +- theories/Bool/DecBool.v | 2 +- theories/Bool/IfProp.v | 2 +- theories/Bool/Sumbool.v | 2 +- theories/Bool/Zerob.v | 2 +- theories/Classes/CEquivalence.v | 2 +- theories/Classes/CMorphisms.v | 2 +- theories/Classes/CRelationClasses.v | 2 +- theories/Classes/DecidableClass.v | 2 +- theories/Classes/EquivDec.v | 2 +- theories/Classes/Equivalence.v | 2 +- theories/Classes/Init.v | 2 +- theories/Classes/Morphisms.v | 2 +- theories/Classes/Morphisms_Prop.v | 2 +- theories/Classes/Morphisms_Relations.v | 2 +- theories/Classes/RelationClasses.v | 2 +- theories/Classes/SetoidClass.v | 2 +- theories/Classes/SetoidDec.v | 2 +- theories/Classes/SetoidTactics.v | 2 +- theories/Compat/AdmitAxiom.v | 2 +- theories/Compat/Coq85.v | 2 +- theories/Compat/Coq86.v | 2 +- theories/Init/Datatypes.v | 2 +- theories/Init/Logic.v | 2 +- theories/Init/Logic_Type.v | 2 +- theories/Init/Nat.v | 2 +- theories/Init/Notations.v | 2 +- theories/Init/Peano.v | 2 +- theories/Init/Prelude.v | 2 +- theories/Init/Specif.v | 2 +- theories/Init/Tactics.v | 2 +- theories/Init/Wf.v | 2 +- theories/Lists/List.v | 2 +- theories/Lists/ListDec.v | 2 +- theories/Lists/ListSet.v | 2 +- theories/Lists/ListTactics.v | 2 +- theories/Lists/StreamMemo.v | 2 +- theories/Lists/Streams.v | 2 +- theories/Logic/Berardi.v | 2 +- theories/Logic/ChoiceFacts.v | 2 +- theories/Logic/Classical.v | 2 +- theories/Logic/ClassicalChoice.v | 2 +- theories/Logic/ClassicalDescription.v | 2 +- theories/Logic/ClassicalEpsilon.v | 2 +- theories/Logic/ClassicalFacts.v | 2 +- theories/Logic/ClassicalUniqueChoice.v | 2 +- theories/Logic/Classical_Pred_Type.v | 2 +- theories/Logic/Classical_Prop.v | 2 +- theories/Logic/ConstructiveEpsilon.v | 2 +- theories/Logic/Decidable.v | 2 +- theories/Logic/Description.v | 2 +- theories/Logic/Diaconescu.v | 2 +- theories/Logic/Epsilon.v | 2 +- theories/Logic/Eqdep.v | 2 +- theories/Logic/EqdepFacts.v | 2 +- theories/Logic/Eqdep_dec.v | 2 +- theories/Logic/ExtensionalFunctionRepresentative.v | 2 +- theories/Logic/ExtensionalityFacts.v | 2 +- theories/Logic/FinFun.v | 2 +- theories/Logic/FunctionalExtensionality.v | 2 +- theories/Logic/Hurkens.v | 2 +- theories/Logic/IndefiniteDescription.v | 2 +- theories/Logic/JMeq.v | 2 +- theories/Logic/ProofIrrelevance.v | 2 +- theories/Logic/ProofIrrelevanceFacts.v | 2 +- theories/Logic/PropExtensionality.v | 2 +- theories/Logic/PropExtensionalityFacts.v | 2 +- theories/Logic/RelationalChoice.v | 2 +- theories/Logic/SetIsType.v | 2 +- theories/Logic/SetoidChoice.v | 2 +- theories/Logic/WKL.v | 2 +- theories/Logic/WeakFan.v | 2 +- theories/NArith/BinNat.v | 2 +- theories/NArith/BinNatDef.v | 2 +- theories/NArith/NArith.v | 2 +- theories/NArith/Ndec.v | 2 +- theories/NArith/Ndigits.v | 2 +- theories/NArith/Ndist.v | 2 +- theories/NArith/Ndiv_def.v | 2 +- theories/NArith/Ngcd_def.v | 2 +- theories/NArith/Nnat.v | 2 +- theories/NArith/Nsqrt_def.v | 2 +- theories/Numbers/BinNums.v | 2 +- theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 2 +- theories/Numbers/Cyclic/Abstract/DoubleType.v | 2 +- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 2 +- theories/Numbers/Cyclic/Int31/Cyclic31.v | 2 +- theories/Numbers/Cyclic/Int31/Int31.v | 2 +- theories/Numbers/Cyclic/Int31/Ring31.v | 2 +- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 2 +- theories/Numbers/Integer/Abstract/ZAdd.v | 2 +- theories/Numbers/Integer/Abstract/ZAddOrder.v | 2 +- theories/Numbers/Integer/Abstract/ZAxioms.v | 2 +- theories/Numbers/Integer/Abstract/ZBase.v | 2 +- theories/Numbers/Integer/Abstract/ZBits.v | 2 +- theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +- theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +- theories/Numbers/Integer/Abstract/ZGcd.v | 2 +- theories/Numbers/Integer/Abstract/ZLcm.v | 2 +- theories/Numbers/Integer/Abstract/ZLt.v | 2 +- theories/Numbers/Integer/Abstract/ZMaxMin.v | 2 +- theories/Numbers/Integer/Abstract/ZMul.v | 2 +- theories/Numbers/Integer/Abstract/ZMulOrder.v | 2 +- theories/Numbers/Integer/Abstract/ZParity.v | 2 +- theories/Numbers/Integer/Abstract/ZPow.v | 2 +- theories/Numbers/Integer/Abstract/ZProperties.v | 2 +- theories/Numbers/Integer/Abstract/ZSgnAbs.v | 2 +- theories/Numbers/Integer/Binary/ZBinary.v | 2 +- theories/Numbers/Integer/NatPairs/ZNatPairs.v | 2 +- theories/Numbers/NaryFunctions.v | 2 +- theories/Numbers/NatInt/NZAdd.v | 2 +- theories/Numbers/NatInt/NZAddOrder.v | 2 +- theories/Numbers/NatInt/NZAxioms.v | 2 +- theories/Numbers/NatInt/NZBase.v | 2 +- theories/Numbers/NatInt/NZBits.v | 2 +- theories/Numbers/NatInt/NZDiv.v | 2 +- theories/Numbers/NatInt/NZDomain.v | 2 +- theories/Numbers/NatInt/NZGcd.v | 2 +- theories/Numbers/NatInt/NZLog.v | 2 +- theories/Numbers/NatInt/NZMul.v | 2 +- theories/Numbers/NatInt/NZMulOrder.v | 2 +- theories/Numbers/NatInt/NZOrder.v | 2 +- theories/Numbers/NatInt/NZParity.v | 2 +- theories/Numbers/NatInt/NZPow.v | 2 +- theories/Numbers/NatInt/NZProperties.v | 2 +- theories/Numbers/NatInt/NZSqrt.v | 2 +- theories/Numbers/Natural/Abstract/NAdd.v | 2 +- theories/Numbers/Natural/Abstract/NAddOrder.v | 2 +- theories/Numbers/Natural/Abstract/NAxioms.v | 2 +- theories/Numbers/Natural/Abstract/NBase.v | 2 +- theories/Numbers/Natural/Abstract/NBits.v | 2 +- theories/Numbers/Natural/Abstract/NDefOps.v | 2 +- theories/Numbers/Natural/Abstract/NDiv.v | 2 +- theories/Numbers/Natural/Abstract/NGcd.v | 2 +- theories/Numbers/Natural/Abstract/NIso.v | 2 +- theories/Numbers/Natural/Abstract/NLcm.v | 2 +- theories/Numbers/Natural/Abstract/NLog.v | 2 +- theories/Numbers/Natural/Abstract/NMaxMin.v | 2 +- theories/Numbers/Natural/Abstract/NMulOrder.v | 2 +- theories/Numbers/Natural/Abstract/NOrder.v | 2 +- theories/Numbers/Natural/Abstract/NParity.v | 2 +- theories/Numbers/Natural/Abstract/NPow.v | 2 +- theories/Numbers/Natural/Abstract/NProperties.v | 2 +- theories/Numbers/Natural/Abstract/NSqrt.v | 2 +- theories/Numbers/Natural/Abstract/NStrongRec.v | 2 +- theories/Numbers/Natural/Abstract/NSub.v | 2 +- theories/Numbers/Natural/Binary/NBinary.v | 2 +- theories/Numbers/Natural/Peano/NPeano.v | 2 +- theories/Numbers/NumPrelude.v | 2 +- theories/PArith/BinPos.v | 2 +- theories/PArith/BinPosDef.v | 2 +- theories/PArith/PArith.v | 2 +- theories/PArith/POrderedType.v | 2 +- theories/PArith/Pnat.v | 2 +- theories/Program/Basics.v | 2 +- theories/Program/Combinators.v | 2 +- theories/Program/Equality.v | 2 +- theories/Program/Program.v | 2 +- theories/Program/Subset.v | 2 +- theories/Program/Syntax.v | 2 +- theories/Program/Tactics.v | 2 +- theories/Program/Utils.v | 2 +- theories/Program/Wf.v | 2 +- theories/QArith/QArith.v | 2 +- theories/QArith/QArith_base.v | 2 +- theories/QArith/QOrderedType.v | 2 +- theories/QArith/Qabs.v | 2 +- theories/QArith/Qcabs.v | 2 +- theories/QArith/Qcanon.v | 2 +- theories/QArith/Qfield.v | 2 +- theories/QArith/Qminmax.v | 2 +- theories/QArith/Qpower.v | 2 +- theories/QArith/Qreals.v | 2 +- theories/QArith/Qreduction.v | 2 +- theories/QArith/Qring.v | 2 +- theories/QArith/Qround.v | 2 +- theories/Reals/Alembert.v | 2 +- theories/Reals/AltSeries.v | 2 +- theories/Reals/ArithProp.v | 2 +- theories/Reals/Binomial.v | 2 +- theories/Reals/Cauchy_prod.v | 2 +- theories/Reals/Cos_plus.v | 2 +- theories/Reals/Cos_rel.v | 2 +- theories/Reals/DiscrR.v | 2 +- theories/Reals/Exp_prop.v | 2 +- theories/Reals/Integration.v | 2 +- theories/Reals/MVT.v | 2 +- theories/Reals/Machin.v | 2 +- theories/Reals/NewtonInt.v | 2 +- theories/Reals/PSeries_reg.v | 2 +- theories/Reals/PartSum.v | 2 +- theories/Reals/RIneq.v | 2 +- theories/Reals/RList.v | 2 +- theories/Reals/ROrderedType.v | 2 +- theories/Reals/R_Ifp.v | 2 +- theories/Reals/R_sqr.v | 2 +- theories/Reals/R_sqrt.v | 2 +- theories/Reals/Ranalysis.v | 2 +- theories/Reals/Ranalysis1.v | 2 +- theories/Reals/Ranalysis2.v | 2 +- theories/Reals/Ranalysis3.v | 2 +- theories/Reals/Ranalysis4.v | 2 +- theories/Reals/Ranalysis5.v | 2 +- theories/Reals/Ranalysis_reg.v | 2 +- theories/Reals/Ratan.v | 2 +- theories/Reals/Raxioms.v | 2 +- theories/Reals/Rbase.v | 2 +- theories/Reals/Rbasic_fun.v | 2 +- theories/Reals/Rcomplete.v | 2 +- theories/Reals/Rdefinitions.v | 2 +- theories/Reals/Rderiv.v | 2 +- theories/Reals/Reals.v | 2 +- theories/Reals/Rfunctions.v | 2 +- theories/Reals/Rgeom.v | 2 +- theories/Reals/RiemannInt.v | 2 +- theories/Reals/RiemannInt_SF.v | 2 +- theories/Reals/Rlimit.v | 2 +- theories/Reals/Rlogic.v | 2 +- theories/Reals/Rminmax.v | 2 +- theories/Reals/Rpow_def.v | 2 +- theories/Reals/Rpower.v | 2 +- theories/Reals/Rprod.v | 2 +- theories/Reals/Rseries.v | 2 +- theories/Reals/Rsigma.v | 2 +- theories/Reals/Rsqrt_def.v | 2 +- theories/Reals/Rtopology.v | 2 +- theories/Reals/Rtrigo.v | 2 +- theories/Reals/Rtrigo1.v | 2 +- theories/Reals/Rtrigo_alt.v | 2 +- theories/Reals/Rtrigo_calc.v | 2 +- theories/Reals/Rtrigo_def.v | 2 +- theories/Reals/Rtrigo_fun.v | 2 +- theories/Reals/Rtrigo_reg.v | 2 +- theories/Reals/SeqProp.v | 2 +- theories/Reals/SeqSeries.v | 2 +- theories/Reals/SplitAbsolu.v | 2 +- theories/Reals/SplitRmult.v | 2 +- theories/Reals/Sqrt_reg.v | 2 +- theories/Relations/Operators_Properties.v | 2 +- theories/Relations/Relation_Definitions.v | 2 +- theories/Relations/Relation_Operators.v | 2 +- theories/Relations/Relations.v | 2 +- theories/Setoids/Setoid.v | 2 +- theories/Sets/Classical_sets.v | 2 +- theories/Sets/Constructive_sets.v | 2 +- theories/Sets/Cpo.v | 2 +- theories/Sets/Ensembles.v | 2 +- theories/Sets/Finite_sets.v | 2 +- theories/Sets/Finite_sets_facts.v | 2 +- theories/Sets/Image.v | 2 +- theories/Sets/Infinite_sets.v | 2 +- theories/Sets/Integers.v | 2 +- theories/Sets/Multiset.v | 2 +- theories/Sets/Partial_Order.v | 2 +- theories/Sets/Permut.v | 2 +- theories/Sets/Powerset.v | 2 +- theories/Sets/Powerset_Classical_facts.v | 2 +- theories/Sets/Powerset_facts.v | 2 +- theories/Sets/Relations_1.v | 2 +- theories/Sets/Relations_1_facts.v | 2 +- theories/Sets/Relations_2.v | 2 +- theories/Sets/Relations_2_facts.v | 2 +- theories/Sets/Relations_3.v | 2 +- theories/Sets/Relations_3_facts.v | 2 +- theories/Sets/Uniset.v | 2 +- theories/Sorting/Heap.v | 2 +- theories/Sorting/Mergesort.v | 2 +- theories/Sorting/PermutEq.v | 2 +- theories/Sorting/PermutSetoid.v | 2 +- theories/Sorting/Permutation.v | 2 +- theories/Sorting/Sorted.v | 2 +- theories/Sorting/Sorting.v | 2 +- theories/Strings/Ascii.v | 2 +- theories/Strings/String.v | 2 +- theories/Unicode/Utf8.v | 2 +- theories/Unicode/Utf8_core.v | 2 +- theories/Wellfounded/Disjoint_Union.v | 2 +- theories/Wellfounded/Inclusion.v | 2 +- theories/Wellfounded/Inverse_Image.v | 2 +- theories/Wellfounded/Lexicographic_Exponentiation.v | 2 +- theories/Wellfounded/Lexicographic_Product.v | 2 +- theories/Wellfounded/Transitive_Closure.v | 2 +- theories/Wellfounded/Union.v | 2 +- theories/Wellfounded/Well_Ordering.v | 2 +- theories/Wellfounded/Wellfounded.v | 2 +- theories/ZArith/BinInt.v | 2 +- theories/ZArith/BinIntDef.v | 2 +- theories/ZArith/Wf_Z.v | 2 +- theories/ZArith/ZArith.v | 2 +- theories/ZArith/ZArith_base.v | 2 +- theories/ZArith/ZArith_dec.v | 2 +- theories/ZArith/Zabs.v | 2 +- theories/ZArith/Zbool.v | 2 +- theories/ZArith/Zcompare.v | 2 +- theories/ZArith/Zcomplements.v | 2 +- theories/ZArith/Zdigits.v | 2 +- theories/ZArith/Zdiv.v | 2 +- theories/ZArith/Zeuclid.v | 2 +- theories/ZArith/Zeven.v | 2 +- theories/ZArith/Zgcd_alt.v | 2 +- theories/ZArith/Zhints.v | 2 +- theories/ZArith/Zlogarithm.v | 2 +- theories/ZArith/Zmax.v | 2 +- theories/ZArith/Zmin.v | 2 +- theories/ZArith/Zminmax.v | 2 +- theories/ZArith/Zmisc.v | 2 +- theories/ZArith/Znat.v | 2 +- theories/ZArith/Znumtheory.v | 2 +- theories/ZArith/Zorder.v | 2 +- theories/ZArith/Zpow_alt.v | 2 +- theories/ZArith/Zpow_def.v | 2 +- theories/ZArith/Zpow_facts.v | 2 +- theories/ZArith/Zpower.v | 2 +- theories/ZArith/Zquot.v | 2 +- theories/ZArith/Zsqrt_compat.v | 2 +- theories/ZArith/Zwf.v | 2 +- theories/ZArith/auxiliary.v | 2 +- tools/coq_makefile.ml | 2 +- tools/coq_tex.ml | 2 +- tools/coqc.ml | 2 +- tools/coqdep.ml | 2 +- tools/coqdep_boot.ml | 2 +- tools/coqdep_common.ml | 2 +- tools/coqdep_common.mli | 2 +- tools/coqdep_lexer.mli | 2 +- tools/coqdep_lexer.mll | 2 +- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 2 +- tools/coqdoc/cpretty.mli | 2 +- tools/coqdoc/cpretty.mll | 2 +- tools/coqdoc/index.ml | 2 +- tools/coqdoc/index.mli | 2 +- tools/coqdoc/main.ml | 2 +- tools/coqdoc/output.ml | 2 +- tools/coqdoc/output.mli | 2 +- tools/coqdoc/tokens.ml | 2 +- tools/coqdoc/tokens.mli | 2 +- tools/coqmktop.ml | 2 +- tools/coqwc.mll | 2 +- tools/coqworkmgr.ml | 2 +- tools/fake_ide.ml | 2 +- tools/gallina.ml | 2 +- tools/gallina_lexer.mll | 2 +- toplevel/coqinit.ml | 2 +- toplevel/coqinit.mli | 2 +- toplevel/coqloop.ml | 2 +- toplevel/coqloop.mli | 2 +- toplevel/coqtop.ml | 2 +- toplevel/coqtop.mli | 2 +- toplevel/usage.ml | 2 +- toplevel/usage.mli | 2 +- toplevel/vernac.ml | 2 +- toplevel/vernac.mli | 2 +- vernac/assumptions.ml | 2 +- vernac/assumptions.mli | 2 +- vernac/auto_ind_decl.ml | 2 +- vernac/auto_ind_decl.mli | 2 +- vernac/class.ml | 2 +- vernac/class.mli | 2 +- vernac/classes.ml | 2 +- vernac/classes.mli | 2 +- vernac/command.ml | 2 +- vernac/command.mli | 2 +- vernac/discharge.ml | 2 +- vernac/discharge.mli | 2 +- vernac/explainErr.ml | 2 +- vernac/explainErr.mli | 2 +- vernac/himsg.ml | 2 +- vernac/himsg.mli | 2 +- vernac/ind_tables.ml | 2 +- vernac/ind_tables.mli | 2 +- vernac/indschemes.ml | 2 +- vernac/indschemes.mli | 2 +- vernac/lemmas.ml | 2 +- vernac/lemmas.mli | 2 +- vernac/locality.ml | 2 +- vernac/locality.mli | 2 +- vernac/metasyntax.ml | 2 +- vernac/metasyntax.mli | 2 +- vernac/mltop.ml | 2 +- vernac/mltop.mli | 2 +- vernac/obligations.mli | 2 +- vernac/record.ml | 2 +- vernac/record.mli | 2 +- vernac/search.ml | 2 +- vernac/search.mli | 2 +- vernac/topfmt.ml | 2 +- vernac/topfmt.mli | 2 +- vernac/vernacentries.ml | 2 +- vernac/vernacentries.mli | 2 +- vernac/vernacinterp.ml | 2 +- vernac/vernacinterp.mli | 2 +- vernac/vernacprop.ml | 2 +- vernac/vernacprop.mli | 2 +- 1171 files changed, 1172 insertions(+), 1172 deletions(-) diff --git a/API/API.ml b/API/API.ml index 29aa1b7a5..093ca97f8 100644 --- a/API/API.ml +++ b/API/API.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*