From 42e09b6d888a29cc6273b8e77d5f9a2e5582abc4 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 6 Jun 2019 11:22:08 +0200 Subject: Update ml-style headers to new year. --- checker/check.ml | 2 +- checker/check.mli | 2 +- checker/checkInductive.ml | 2 +- checker/checkInductive.mli | 2 +- checker/checkTypes.ml | 2 +- checker/checkTypes.mli | 2 +- checker/check_stat.ml | 2 +- checker/check_stat.mli | 2 +- checker/checker.ml | 2 +- checker/checker.mli | 2 +- checker/coqchk.mli | 2 +- checker/mod_checking.mli | 2 +- checker/safe_checking.ml | 2 +- checker/safe_checking.mli | 2 +- checker/validate.ml | 2 +- checker/validate.mli | 2 +- checker/values.ml | 2 +- checker/values.mli | 2 +- checker/votour.ml | 2 +- checker/votour.mli | 2 +- clib/backtrace.ml | 2 +- clib/backtrace.mli | 2 +- clib/bigint.ml | 2 +- clib/bigint.mli | 2 +- clib/cArray.ml | 2 +- clib/cArray.mli | 2 +- clib/cEphemeron.ml | 2 +- clib/cEphemeron.mli | 2 +- clib/cList.ml | 2 +- clib/cList.mli | 2 +- clib/cMap.ml | 2 +- clib/cMap.mli | 2 +- clib/cObj.ml | 2 +- clib/cObj.mli | 2 +- clib/cSet.ml | 2 +- clib/cSet.mli | 2 +- clib/cSig.mli | 2 +- clib/cStack.ml | 2 +- clib/cStack.mli | 2 +- clib/cString.ml | 2 +- clib/cString.mli | 2 +- clib/cThread.ml | 2 +- clib/cThread.mli | 2 +- clib/cUnix.ml | 2 +- clib/cUnix.mli | 2 +- clib/dyn.ml | 2 +- clib/dyn.mli | 2 +- clib/exninfo.ml | 2 +- clib/exninfo.mli | 2 +- clib/hMap.ml | 2 +- clib/hMap.mli | 2 +- clib/hashcons.ml | 2 +- clib/hashcons.mli | 2 +- clib/hashset.ml | 2 +- clib/hashset.mli | 2 +- clib/heap.ml | 2 +- clib/heap.mli | 2 +- clib/iStream.ml | 2 +- clib/iStream.mli | 2 +- clib/int.ml | 2 +- clib/int.mli | 2 +- clib/minisys.ml | 2 +- clib/monad.ml | 2 +- clib/monad.mli | 2 +- clib/option.ml | 2 +- clib/option.mli | 2 +- clib/orderedType.ml | 2 +- clib/orderedType.mli | 2 +- clib/range.ml | 2 +- clib/range.mli | 2 +- clib/segmenttree.ml | 2 +- clib/segmenttree.mli | 2 +- clib/store.ml | 2 +- clib/store.mli | 2 +- clib/terminal.ml | 2 +- clib/terminal.mli | 2 +- clib/trie.ml | 2 +- clib/trie.mli | 2 +- clib/unicode.ml | 2 +- clib/unicode.mli | 2 +- clib/unionfind.ml | 2 +- clib/unionfind.mli | 2 +- config/coq_config.mli | 2 +- dev/header.ml | 2 +- dev/top_printers.ml | 2 +- dev/top_printers.mli | 2 +- engine/eConstr.ml | 2 +- engine/eConstr.mli | 2 +- engine/evar_kinds.ml | 2 +- engine/evar_kinds.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/logic_monad.ml | 2 +- engine/logic_monad.mli | 2 +- engine/namegen.ml | 2 +- engine/namegen.mli | 2 +- engine/nameops.ml | 2 +- engine/nameops.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/uState.ml | 2 +- engine/uState.mli | 2 +- engine/univGen.ml | 2 +- engine/univGen.mli | 2 +- engine/univMinim.ml | 2 +- engine/univMinim.mli | 2 +- engine/univNames.ml | 2 +- engine/univNames.mli | 2 +- engine/univProblem.ml | 2 +- engine/univProblem.mli | 2 +- engine/univSubst.ml | 2 +- engine/univSubst.mli | 2 +- engine/univops.ml | 2 +- engine/univops.mli | 2 +- ide/config_lexer.mli | 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_commands.mli | 2 +- ide/coq_lex.mli | 2 +- ide/coq_lex.mll | 2 +- ide/coqide.ml | 2 +- ide/coqide.mli | 2 +- ide/coqide_QUARTZ.ml.in | 2 +- ide/coqide_WIN32.ml.in | 2 +- ide/coqide_X11.ml.in | 2 +- ide/coqide_main.ml | 2 +- ide/coqide_main.mli | 2 +- ide/coqide_os_specific.mli | 2 +- ide/coqide_ui.mli | 2 +- ide/document.ml | 2 +- ide/document.mli | 2 +- ide/fake_ide.ml | 2 +- ide/fileOps.ml | 2 +- ide/fileOps.mli | 2 +- ide/gtk_parsing.ml | 2 +- ide/gtk_parsing.mli | 2 +- ide/idetop.ml | 2 +- ide/ideutils.ml | 2 +- ide/ideutils.mli | 2 +- ide/macos_prehook.mli | 2 +- ide/microPG.ml | 2 +- ide/microPG.mli | 2 +- ide/minilib.ml | 2 +- ide/minilib.mli | 2 +- ide/preferences.ml | 2 +- ide/preferences.mli | 2 +- ide/protocol/interface.ml | 2 +- ide/protocol/richpp.ml | 2 +- ide/protocol/richpp.mli | 2 +- ide/protocol/serialize.ml | 2 +- ide/protocol/serialize.mli | 2 +- ide/protocol/xml_printer.ml | 2 +- ide/protocol/xml_printer.mli | 2 +- ide/protocol/xmlprotocol.ml | 2 +- ide/protocol/xmlprotocol.mli | 2 +- ide/sentence.ml | 2 +- ide/sentence.mli | 2 +- ide/session.ml | 2 +- ide/session.mli | 2 +- ide/tags.ml | 2 +- ide/tags.mli | 2 +- ide/unicode_bindings.ml | 2 +- ide/unicode_bindings.mli | 2 +- ide/utf8_convert.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_RoutedMessageViews.ml | 2 +- ide/wg_RoutedMessageViews.mli | 2 +- ide/wg_ScriptView.ml | 2 +- ide/wg_ScriptView.mli | 2 +- ide/wg_Segment.ml | 2 +- ide/wg_Segment.mli | 2 +- interp/constrexpr.ml | 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/declare.ml | 2 +- interp/declare.mli | 2 +- interp/deprecation.ml | 2 +- interp/deprecation.mli | 2 +- interp/dumpglob.ml | 2 +- interp/dumpglob.mli | 2 +- interp/genintern.ml | 2 +- interp/genintern.mli | 2 +- interp/impargs.ml | 2 +- interp/impargs.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/notation_term.ml | 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 +- kernel/cClosure.ml | 2 +- kernel/cClosure.mli | 2 +- kernel/cPrimitives.ml | 2 +- kernel/cPrimitives.mli | 2 +- kernel/cbytecodes.ml | 2 +- kernel/cbytecodes.mli | 2 +- kernel/cbytegen.ml | 2 +- kernel/cbytegen.mli | 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.ml | 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/genOpcodeFiles.ml | 2 +- kernel/indTyping.ml | 2 +- kernel/indTyping.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/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/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/transparentState.ml | 2 +- kernel/transparentState.mli | 2 +- kernel/type_errors.ml | 2 +- kernel/type_errors.mli | 2 +- kernel/typeops.ml | 2 +- kernel/typeops.mli | 2 +- kernel/uGraph.ml | 2 +- kernel/uGraph.mli | 2 +- kernel/uint63_amd64_63.ml | 2 +- kernel/uint63_i386_31.ml | 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 +- kernel/vm.mli | 2 +- kernel/vmvalues.ml | 2 +- kernel/vmvalues.mli | 2 +- kernel/write_uint63.ml | 2 +- lib/acyclicGraph.ml | 2 +- lib/acyclicGraph.mli | 2 +- lib/aux_file.ml | 2 +- lib/aux_file.mli | 2 +- lib/cAst.ml | 2 +- lib/cAst.mli | 2 +- lib/cErrors.ml | 2 +- lib/cErrors.mli | 2 +- lib/cProfile.ml | 2 +- lib/cProfile.mli | 2 +- lib/cWarnings.ml | 2 +- lib/cWarnings.mli | 2 +- lib/control.ml | 2 +- lib/control.mli | 2 +- lib/coqProject_file.ml | 2 +- lib/coqProject_file.mli | 2 +- lib/dAst.ml | 2 +- lib/dAst.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/hook.ml | 2 +- lib/hook.mli | 2 +- lib/loc.ml | 2 +- lib/loc.mli | 2 +- lib/pp.ml | 2 +- lib/pp.mli | 2 +- lib/pp_diff.ml | 2 +- lib/pp_diff.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/stateid.ml | 2 +- lib/stateid.mli | 2 +- lib/system.ml | 2 +- lib/system.mli | 2 +- lib/util.ml | 2 +- lib/util.mli | 2 +- lib/xml_datatype.mli | 2 +- library/coqlib.ml | 2 +- library/coqlib.mli | 2 +- library/decl_kinds.ml | 2 +- library/declaremods.ml | 2 +- library/declaremods.mli | 2 +- library/decls.ml | 2 +- library/decls.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/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/nametab.ml | 2 +- library/nametab.mli | 2 +- library/states.ml | 2 +- library/states.mli | 2 +- library/summary.ml | 2 +- library/summary.mli | 2 +- parsing/cLexer.ml | 2 +- parsing/cLexer.mli | 2 +- parsing/extend.ml | 2 +- parsing/g_constr.mlg | 2 +- parsing/g_prim.mlg | 2 +- parsing/notation_gram.ml | 2 +- parsing/notgram_ops.ml | 2 +- parsing/notgram_ops.mli | 2 +- parsing/pcoq.ml | 2 +- parsing/pcoq.mli | 2 +- parsing/ppextend.ml | 2 +- parsing/ppextend.mli | 2 +- parsing/tok.ml | 2 +- parsing/tok.mli | 2 +- plugins/btauto/g_btauto.mlg | 2 +- plugins/btauto/refl_btauto.ml | 2 +- plugins/btauto/refl_btauto.mli | 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/cctac.mli | 2 +- plugins/cc/g_congruence.mlg | 2 +- plugins/derive/derive.ml | 2 +- plugins/derive/derive.mli | 2 +- plugins/derive/g_derive.mlg | 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.mlg | 2 +- plugins/extraction/haskell.ml | 2 +- plugins/extraction/haskell.mli | 2 +- plugins/extraction/miniml.ml | 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.mlg | 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/funind/FunInd.v | 2 +- plugins/funind/Recdef.v | 2 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/functional_principles_types.mli | 2 +- plugins/funind/g_indfun.mlg | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/invfun.mli | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ltac/coretactics.mlg | 2 +- plugins/ltac/evar_tactics.ml | 2 +- plugins/ltac/evar_tactics.mli | 2 +- plugins/ltac/extraargs.mlg | 2 +- plugins/ltac/extraargs.mli | 2 +- plugins/ltac/extratactics.mlg | 2 +- plugins/ltac/extratactics.mli | 2 +- plugins/ltac/g_auto.mlg | 2 +- plugins/ltac/g_class.mlg | 2 +- plugins/ltac/g_eqdecide.mlg | 2 +- plugins/ltac/g_ltac.mlg | 2 +- plugins/ltac/g_obligations.mlg | 2 +- plugins/ltac/g_rewrite.mlg | 2 +- plugins/ltac/g_tactic.mlg | 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.mlg | 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.ml | 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_matching.mli | 2 +- plugins/ltac/tactic_option.ml | 2 +- plugins/ltac/tactic_option.mli | 2 +- plugins/ltac/tauto.ml | 2 +- plugins/micromega/DeclConstant.v | 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/certificate.mli | 2 +- plugins/micromega/coq_micromega.ml | 2 +- plugins/micromega/coq_micromega.mli | 2 +- plugins/micromega/csdpcert.ml | 2 +- plugins/micromega/csdpcert.mli | 2 +- plugins/micromega/g_micromega.mlg | 2 +- plugins/micromega/g_micromega.mli | 2 +- plugins/micromega/itv.ml | 2 +- plugins/micromega/itv.mli | 2 +- plugins/micromega/mfourier.ml | 2 +- plugins/micromega/mfourier.mli | 2 +- plugins/micromega/mutils.ml | 2 +- plugins/micromega/mutils.mli | 2 +- plugins/micromega/persistent_cache.ml | 2 +- plugins/micromega/persistent_cache.mli | 2 +- plugins/micromega/polynomial.ml | 2 +- plugins/micromega/polynomial.mli | 2 +- plugins/micromega/simplex.ml | 2 +- plugins/micromega/simplex.mli | 2 +- plugins/micromega/sos.mli | 2 +- plugins/micromega/sos_lib.mli | 2 +- plugins/micromega/sos_types.ml | 2 +- plugins/micromega/sos_types.mli | 2 +- plugins/micromega/vect.ml | 2 +- plugins/micromega/vect.mli | 2 +- plugins/nsatz/Nsatz.v | 2 +- plugins/nsatz/g_nsatz.mlg | 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/OmegaLemmas.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/coq_omega.mli | 2 +- plugins/omega/g_omega.mlg | 2 +- plugins/omega/omega.ml | 2 +- plugins/rtauto/Bintree.v | 2 +- plugins/rtauto/Rtauto.v | 2 +- plugins/rtauto/g_rtauto.mlg | 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/Algebra_syntax.v | 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/Integral_domain.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/RealField.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_tac.v | 2 +- plugins/setoid_ring/Ring_theory.v | 2 +- plugins/setoid_ring/Rings_Q.v | 2 +- plugins/setoid_ring/Rings_R.v | 2 +- plugins/setoid_ring/Rings_Z.v | 2 +- plugins/setoid_ring/ZArithRing.v | 2 +- plugins/setoid_ring/g_newring.mlg | 2 +- plugins/setoid_ring/newring.ml | 2 +- plugins/setoid_ring/newring.mli | 2 +- plugins/setoid_ring/newring_ast.ml | 2 +- plugins/setoid_ring/newring_ast.mli | 2 +- plugins/ssr/ssrast.mli | 2 +- plugins/ssr/ssrbool.v | 2 +- plugins/ssr/ssrbwd.ml | 2 +- plugins/ssr/ssrbwd.mli | 2 +- plugins/ssr/ssrcommon.ml | 2 +- plugins/ssr/ssrcommon.mli | 2 +- plugins/ssr/ssreflect.v | 2 +- plugins/ssr/ssrelim.ml | 2 +- plugins/ssr/ssrelim.mli | 2 +- plugins/ssr/ssrequality.ml | 2 +- plugins/ssr/ssrequality.mli | 2 +- plugins/ssr/ssrfun.v | 2 +- plugins/ssr/ssrfwd.ml | 2 +- plugins/ssr/ssrfwd.mli | 2 +- plugins/ssr/ssripats.ml | 2 +- plugins/ssr/ssripats.mli | 2 +- plugins/ssr/ssrparser.mlg | 2 +- plugins/ssr/ssrparser.mli | 2 +- plugins/ssr/ssrprinters.ml | 2 +- plugins/ssr/ssrprinters.mli | 2 +- plugins/ssr/ssrtacticals.ml | 2 +- plugins/ssr/ssrtacticals.mli | 2 +- plugins/ssr/ssrvernac.mlg | 2 +- plugins/ssr/ssrvernac.mli | 2 +- plugins/ssr/ssrview.ml | 2 +- plugins/ssr/ssrview.mli | 2 +- plugins/ssrmatching/g_ssrmatching.mlg | 2 +- plugins/ssrmatching/g_ssrmatching.mli | 2 +- plugins/ssrmatching/ssrmatching.ml | 2 +- plugins/ssrmatching/ssrmatching.mli | 2 +- plugins/ssrmatching/ssrmatching.v | 2 +- plugins/syntax/g_numeral.mlg | 2 +- plugins/syntax/g_string.mlg | 2 +- plugins/syntax/numeral.ml | 2 +- plugins/syntax/numeral.mli | 2 +- plugins/syntax/r_syntax.ml | 2 +- plugins/syntax/r_syntax.mli | 2 +- plugins/syntax/string_notation.ml | 2 +- plugins/syntax/string_notation.mli | 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/geninterp.ml | 2 +- pretyping/geninterp.mli | 2 +- pretyping/globEnv.ml | 2 +- pretyping/globEnv.mli | 2 +- pretyping/glob_ops.ml | 2 +- pretyping/glob_ops.mli | 2 +- pretyping/glob_term.ml | 2 +- pretyping/heads.ml | 2 +- pretyping/heads.mli | 2 +- pretyping/indrec.ml | 2 +- pretyping/indrec.mli | 2 +- pretyping/inductiveops.ml | 2 +- pretyping/inductiveops.mli | 2 +- pretyping/inferCumulativity.ml | 2 +- pretyping/inferCumulativity.mli | 2 +- pretyping/locus.ml | 2 +- pretyping/locusops.ml | 2 +- pretyping/locusops.mli | 2 +- pretyping/nativenorm.ml | 2 +- pretyping/nativenorm.mli | 2 +- pretyping/pattern.ml | 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/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/ppconstr.ml | 2 +- printing/ppconstr.mli | 2 +- printing/pputils.ml | 2 +- printing/pputils.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 +- printing/proof_diffs.ml | 2 +- printing/proof_diffs.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/goal_select.ml | 2 +- proofs/goal_select.mli | 2 +- proofs/logic.ml | 2 +- proofs/logic.mli | 2 +- proofs/miscprint.ml | 2 +- proofs/miscprint.mli | 2 +- proofs/pfedit.ml | 2 +- proofs/pfedit.mli | 2 +- proofs/proof.ml | 2 +- proofs/proof.mli | 2 +- proofs/proof_bullet.ml | 2 +- proofs/proof_bullet.mli | 2 +- proofs/proof_global.ml | 2 +- proofs/proof_global.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 +- proofs/tactypes.ml | 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/spawned.ml | 2 +- stm/spawned.mli | 2 +- stm/stm.ml | 2 +- stm/stm.mli | 2 +- stm/tQueue.ml | 2 +- stm/tQueue.mli | 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/workerPool.ml | 2 +- stm/workerPool.mli | 2 +- tactics/abstract.ml | 2 +- tactics/abstract.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/genredexpr.ml | 2 +- tactics/hints.ml | 2 +- tactics/hints.mli | 2 +- tactics/hipattern.ml | 2 +- tactics/hipattern.mli | 2 +- tactics/ind_tables.ml | 2 +- tactics/ind_tables.mli | 2 +- tactics/inv.ml | 2 +- tactics/inv.mli | 2 +- tactics/leminv.ml | 2 +- tactics/leminv.mli | 2 +- tactics/redexpr.ml | 2 +- tactics/redexpr.mli | 2 +- tactics/redops.ml | 2 +- tactics/redops.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/output/ssr_explain_match.v | 2 +- test-suite/prerequisite/ssr_mini_mathcomp.v | 2 +- test-suite/prerequisite/ssr_ssrsyntax1.v | 2 +- test-suite/ssr/absevarprop.v | 2 +- test-suite/ssr/abstract_var2.v | 2 +- test-suite/ssr/binders.v | 2 +- test-suite/ssr/binders_of.v | 2 +- test-suite/ssr/caseview.v | 2 +- test-suite/ssr/congr.v | 2 +- test-suite/ssr/deferclear.v | 2 +- test-suite/ssr/dependent_type_err.v | 2 +- test-suite/ssr/derive_inversion.v | 2 +- test-suite/ssr/elim.v | 2 +- test-suite/ssr/elim2.v | 2 +- test-suite/ssr/elim_pattern.v | 2 +- test-suite/ssr/first_n.v | 2 +- test-suite/ssr/gen_have.v | 2 +- test-suite/ssr/gen_pattern.v | 2 +- test-suite/ssr/have_TC.v | 2 +- test-suite/ssr/have_transp.v | 2 +- test-suite/ssr/have_view_idiom.v | 2 +- test-suite/ssr/havesuff.v | 2 +- test-suite/ssr/if_isnt.v | 2 +- test-suite/ssr/intro_beta.v | 2 +- test-suite/ssr/intro_noop.v | 2 +- test-suite/ssr/ipatalternation.v | 2 +- test-suite/ssr/ltac_have.v | 2 +- test-suite/ssr/ltac_in.v | 2 +- test-suite/ssr/move_after.v | 2 +- test-suite/ssr/multiview.v | 2 +- test-suite/ssr/occarrow.v | 2 +- test-suite/ssr/patnoX.v | 2 +- test-suite/ssr/pattern.v | 2 +- test-suite/ssr/primproj.v | 2 +- test-suite/ssr/rewpatterns.v | 2 +- test-suite/ssr/set_lamda.v | 2 +- test-suite/ssr/set_pattern.v | 2 +- test-suite/ssr/ssrsyntax2.v | 2 +- test-suite/ssr/tc.v | 2 +- test-suite/ssr/typeof.v | 2 +- test-suite/ssr/unfold_Opaque.v | 2 +- test-suite/ssr/unkeyed.v | 2 +- test-suite/ssr/view_case.v | 2 +- test-suite/ssr/wlog_suff.v | 2 +- test-suite/ssr/wlogletin.v | 2 +- test-suite/ssr/wlong_intro.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/Plus.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/RelationPairs.v | 2 +- theories/Classes/SetoidClass.v | 2 +- theories/Classes/SetoidDec.v | 2 +- theories/Classes/SetoidTactics.v | 2 +- theories/Compat/AdmitAxiom.v | 2 +- theories/Compat/Coq810.v | 2 +- theories/Compat/Coq88.v | 2 +- theories/Compat/Coq89.v | 2 +- theories/FSets/FMapAVL.v | 2 +- theories/FSets/FMapFacts.v | 2 +- theories/FSets/FMapFullAVL.v | 2 +- theories/FSets/FMapInterface.v | 2 +- theories/FSets/FMapList.v | 2 +- theories/FSets/FMapPositive.v | 2 +- theories/FSets/FMapWeakList.v | 2 +- theories/FSets/FMaps.v | 2 +- theories/FSets/FSetAVL.v | 2 +- theories/FSets/FSetBridge.v | 2 +- theories/FSets/FSetCompat.v | 2 +- theories/FSets/FSetDecide.v | 2 +- theories/FSets/FSetEqProperties.v | 2 +- theories/FSets/FSetFacts.v | 2 +- theories/FSets/FSetInterface.v | 2 +- theories/FSets/FSetList.v | 2 +- theories/FSets/FSetPositive.v | 2 +- theories/FSets/FSetProperties.v | 2 +- theories/FSets/FSetToFiniteSet.v | 2 +- theories/FSets/FSetWeakList.v | 2 +- theories/FSets/FSets.v | 2 +- theories/Init/Byte.v | 2 +- theories/Init/Datatypes.v | 2 +- theories/Init/Decimal.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/SetoidList.v | 2 +- theories/Lists/SetoidPermutation.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/PropFacts.v | 2 +- theories/Logic/RelationalChoice.v | 2 +- theories/Logic/SetIsType.v | 2 +- theories/Logic/SetoidChoice.v | 2 +- theories/Logic/StrictProp.v | 2 +- theories/Logic/WKL.v | 2 +- theories/Logic/WeakFan.v | 2 +- theories/MSets/MSetAVL.v | 2 +- theories/MSets/MSetDecide.v | 2 +- theories/MSets/MSetEqProperties.v | 2 +- theories/MSets/MSetFacts.v | 2 +- theories/MSets/MSetGenTree.v | 2 +- theories/MSets/MSetInterface.v | 2 +- theories/MSets/MSetList.v | 2 +- theories/MSets/MSetPositive.v | 2 +- theories/MSets/MSetProperties.v | 2 +- theories/MSets/MSetRBT.v | 2 +- theories/MSets/MSetToFiniteSet.v | 2 +- theories/MSets/MSetWeakList.v | 2 +- theories/MSets/MSets.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/AltBinNotations.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/Int63/Int63.v | 2 +- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 2 +- theories/Numbers/DecimalFacts.v | 2 +- theories/Numbers/DecimalN.v | 2 +- theories/Numbers/DecimalNat.v | 2 +- theories/Numbers/DecimalPos.v | 2 +- theories/Numbers/DecimalString.v | 2 +- theories/Numbers/DecimalZ.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/Runcountable.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/Byte.v | 2 +- theories/Strings/ByteVector.v | 2 +- theories/Strings/String.v | 2 +- theories/Structures/DecidableType.v | 2 +- theories/Structures/DecidableTypeEx.v | 2 +- theories/Structures/Equalities.v | 2 +- theories/Structures/EqualitiesFacts.v | 2 +- theories/Structures/GenericMinMax.v | 2 +- theories/Structures/OrderedType.v | 2 +- theories/Structures/OrderedTypeAlt.v | 2 +- theories/Structures/OrderedTypeEx.v | 2 +- theories/Structures/Orders.v | 2 +- theories/Structures/OrdersAlt.v | 2 +- theories/Structures/OrdersEx.v | 2 +- theories/Structures/OrdersFacts.v | 2 +- theories/Structures/OrdersLists.v | 2 +- theories/Structures/OrdersTac.v | 2 +- theories/Unicode/Utf8.v | 2 +- theories/Unicode/Utf8_core.v | 2 +- theories/Vectors/Fin.v | 2 +- theories/Vectors/Vector.v | 2 +- theories/Vectors/VectorDef.v | 2 +- theories/Vectors/VectorEq.v | 2 +- theories/Vectors/VectorSpec.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/Int.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_dune.ml | 2 +- tools/coq_makefile.ml | 2 +- tools/coq_tex.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/coqwc.mll | 2 +- tools/coqworkmgr.ml | 2 +- tools/ocamllibdep.mll | 2 +- topbin/coqc_bin.ml | 2 +- topbin/coqproofworker_bin.ml | 2 +- topbin/coqqueryworker_bin.ml | 2 +- topbin/coqtacticworker_bin.ml | 2 +- topbin/coqtop_bin.ml | 2 +- topbin/coqtop_byte_bin.ml | 2 +- toplevel/ccompile.ml | 2 +- toplevel/ccompile.mli | 2 +- toplevel/coqargs.ml | 2 +- toplevel/coqargs.mli | 2 +- toplevel/coqc.ml | 2 +- toplevel/coqc.mli | 2 +- toplevel/coqcargs.ml | 2 +- toplevel/coqcargs.mli | 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/g_toplevel.mlg | 2 +- toplevel/usage.ml | 2 +- toplevel/usage.mli | 2 +- toplevel/vernac.ml | 2 +- toplevel/vernac.mli | 2 +- toplevel/workerLoop.ml | 2 +- toplevel/workerLoop.mli | 2 +- vernac/assumptions.ml | 2 +- vernac/assumptions.mli | 2 +- vernac/attributes.ml | 2 +- vernac/attributes.mli | 2 +- vernac/auto_ind_decl.ml | 2 +- vernac/auto_ind_decl.mli | 2 +- vernac/canonical.ml | 2 +- vernac/canonical.mli | 2 +- vernac/class.ml | 2 +- vernac/class.mli | 2 +- vernac/classes.ml | 2 +- vernac/classes.mli | 2 +- vernac/comAssumption.ml | 2 +- vernac/comAssumption.mli | 2 +- vernac/comDefinition.ml | 2 +- vernac/comDefinition.mli | 2 +- vernac/comFixpoint.ml | 2 +- vernac/comFixpoint.mli | 2 +- vernac/comInductive.ml | 2 +- vernac/comInductive.mli | 2 +- vernac/comProgramFixpoint.ml | 2 +- vernac/declareDef.ml | 2 +- vernac/declareDef.mli | 2 +- vernac/egramcoq.ml | 2 +- vernac/egramcoq.mli | 2 +- vernac/egramml.ml | 2 +- vernac/egramml.mli | 2 +- vernac/explainErr.ml | 2 +- vernac/explainErr.mli | 2 +- vernac/g_proofs.mlg | 2 +- vernac/g_vernac.mlg | 2 +- vernac/himsg.ml | 2 +- vernac/himsg.mli | 2 +- vernac/indschemes.ml | 2 +- vernac/indschemes.mli | 2 +- vernac/lemmas.ml | 2 +- vernac/lemmas.mli | 2 +- vernac/loadpath.ml | 2 +- vernac/loadpath.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/ppvernac.ml | 2 +- vernac/ppvernac.mli | 2 +- vernac/proof_using.ml | 2 +- vernac/proof_using.mli | 2 +- vernac/pvernac.ml | 2 +- vernac/pvernac.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/vernacexpr.ml | 2 +- vernac/vernacextend.ml | 2 +- vernac/vernacextend.mli | 2 +- vernac/vernacprop.ml | 2 +- vernac/vernacprop.mli | 2 +- vernac/vernacstate.ml | 2 +- vernac/vernacstate.mli | 2 +- 1445 files changed, 1445 insertions(+), 1445 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index 903258daef..918d8ce08e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (*