From a99776e10e0b2198d2b811ad82631111fb450f8a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 18 Mar 2020 12:14:26 +0100 Subject: Update headers in the whole code base. Add headers to a few files which were missing them. --- Makefile | 4 ++-- Makefile.build | 4 ++-- Makefile.checker | 4 ++-- Makefile.ci | 4 ++-- Makefile.common | 4 ++-- Makefile.dev | 4 ++-- Makefile.doc | 4 ++-- Makefile.ide | 4 ++-- Makefile.install | 4 ++-- Makefile.make | 4 ++-- Makefile.vofiles | 9 +++++++++ checker/check.ml | 4 ++-- checker/check.mli | 4 ++-- checker/checkInductive.ml | 4 ++-- checker/checkInductive.mli | 4 ++-- checker/checkTypes.ml | 4 ++-- checker/checkTypes.mli | 4 ++-- checker/check_stat.ml | 4 ++-- checker/check_stat.mli | 4 ++-- checker/checker.ml | 4 ++-- checker/checker.mli | 4 ++-- checker/coqchk.mli | 4 ++-- checker/mod_checking.mli | 4 ++-- checker/safe_checking.ml | 4 ++-- checker/safe_checking.mli | 4 ++-- checker/validate.ml | 4 ++-- checker/validate.mli | 4 ++-- checker/values.ml | 4 ++-- checker/values.mli | 4 ++-- checker/votour.ml | 4 ++-- checker/votour.mli | 4 ++-- clib/bigint.ml | 4 ++-- clib/bigint.mli | 4 ++-- clib/cArray.ml | 4 ++-- clib/cArray.mli | 4 ++-- clib/cEphemeron.ml | 4 ++-- clib/cEphemeron.mli | 4 ++-- clib/cList.ml | 4 ++-- clib/cList.mli | 4 ++-- clib/cMap.ml | 4 ++-- clib/cMap.mli | 4 ++-- clib/cObj.ml | 4 ++-- clib/cObj.mli | 4 ++-- clib/cSet.ml | 4 ++-- clib/cSet.mli | 4 ++-- clib/cSig.mli | 4 ++-- clib/cString.ml | 4 ++-- clib/cString.mli | 4 ++-- clib/cThread.ml | 4 ++-- clib/cThread.mli | 4 ++-- clib/cUnix.ml | 4 ++-- clib/cUnix.mli | 4 ++-- clib/dyn.ml | 4 ++-- clib/dyn.mli | 4 ++-- clib/exninfo.ml | 4 ++-- clib/exninfo.mli | 4 ++-- clib/hMap.ml | 4 ++-- clib/hMap.mli | 4 ++-- clib/hashcons.ml | 4 ++-- clib/hashcons.mli | 4 ++-- clib/hashset.ml | 4 ++-- clib/hashset.mli | 4 ++-- clib/heap.ml | 4 ++-- clib/heap.mli | 4 ++-- clib/iStream.ml | 4 ++-- clib/iStream.mli | 4 ++-- clib/int.ml | 4 ++-- clib/int.mli | 4 ++-- clib/minisys.ml | 4 ++-- clib/monad.ml | 4 ++-- clib/monad.mli | 4 ++-- clib/option.ml | 4 ++-- clib/option.mli | 4 ++-- clib/orderedType.ml | 4 ++-- clib/orderedType.mli | 4 ++-- clib/predicate.ml | 10 ++++++++++ clib/range.ml | 4 ++-- clib/range.mli | 4 ++-- clib/segmenttree.ml | 4 ++-- clib/segmenttree.mli | 4 ++-- clib/store.ml | 4 ++-- clib/store.mli | 4 ++-- clib/terminal.ml | 4 ++-- clib/terminal.mli | 4 ++-- clib/trie.ml | 4 ++-- clib/trie.mli | 4 ++-- clib/unicode.ml | 4 ++-- clib/unicode.mli | 4 ++-- clib/unionfind.ml | 4 ++-- clib/unionfind.mli | 4 ++-- config/coq_config.mli | 4 ++-- coqpp/coqpp_ast.mli | 4 ++-- coqpp/coqpp_lex.mll | 4 ++-- coqpp/coqpp_main.ml | 4 ++-- coqpp/coqpp_parse.mly | 4 ++-- coqpp/coqpp_parser.ml | 4 ++-- coqpp/coqpp_parser.mli | 4 ++-- dev/top_printers.ml | 4 ++-- dev/top_printers.mli | 4 ++-- doc/sphinx/_static/ansi-dark.css | 4 ++-- doc/sphinx/_static/ansi.css | 4 ++-- doc/sphinx/_static/coqdoc.css | 4 ++-- doc/sphinx/_static/notations.css | 4 ++-- doc/sphinx/_static/notations.js | 4 ++-- doc/sphinx/_static/pre-text.css | 4 ++-- doc/sphinx/conf.py | 4 ++-- doc/sphinx/coqdoc.css | 4 ++-- doc/tools/coqrst/__init__.py | 4 ++-- doc/tools/coqrst/checkdeps.py | 4 ++-- doc/tools/coqrst/coqdoc/__init__.py | 4 ++-- doc/tools/coqrst/coqdoc/main.py | 4 ++-- doc/tools/coqrst/coqdomain.py | 4 ++-- doc/tools/coqrst/notations/Makefile | 4 ++-- doc/tools/coqrst/notations/TacticNotations.g | 4 ++-- doc/tools/coqrst/notations/fontsupport.py | 4 ++-- doc/tools/coqrst/notations/html.py | 4 ++-- doc/tools/coqrst/notations/parsing.py | 4 ++-- doc/tools/coqrst/notations/plain.py | 4 ++-- doc/tools/coqrst/notations/regexp.py | 4 ++-- doc/tools/coqrst/notations/sphinx.py | 4 ++-- doc/tools/coqrst/repl/ansicolors.py | 4 ++-- doc/tools/coqrst/repl/coqtop.py | 4 ++-- doc/tools/docgram/common.edit_mlg | 4 ++-- doc/tools/docgram/doc_grammar.ml | 4 ++-- doc/tools/docgram/prodn.edit_mlg | 4 ++-- doc/tools/docgram/productionlist.edit_mlg | 4 ++-- engine/eConstr.ml | 4 ++-- engine/eConstr.mli | 4 ++-- engine/evar_kinds.ml | 4 ++-- engine/evar_kinds.mli | 4 ++-- engine/evarutil.ml | 4 ++-- engine/evarutil.mli | 4 ++-- engine/evd.ml | 4 ++-- engine/evd.mli | 4 ++-- engine/ftactic.ml | 4 ++-- engine/ftactic.mli | 4 ++-- engine/logic_monad.ml | 4 ++-- engine/logic_monad.mli | 4 ++-- engine/namegen.ml | 4 ++-- engine/namegen.mli | 4 ++-- engine/nameops.ml | 4 ++-- engine/nameops.mli | 4 ++-- engine/proofview.ml | 4 ++-- engine/proofview.mli | 4 ++-- engine/proofview_monad.ml | 4 ++-- engine/proofview_monad.mli | 4 ++-- engine/termops.ml | 4 ++-- engine/termops.mli | 4 ++-- engine/uState.ml | 4 ++-- engine/uState.mli | 4 ++-- engine/univGen.ml | 4 ++-- engine/univGen.mli | 4 ++-- engine/univMinim.ml | 4 ++-- engine/univMinim.mli | 4 ++-- engine/univNames.ml | 4 ++-- engine/univNames.mli | 4 ++-- engine/univProblem.ml | 4 ++-- engine/univProblem.mli | 4 ++-- engine/univSubst.ml | 4 ++-- engine/univSubst.mli | 4 ++-- engine/univops.ml | 4 ++-- engine/univops.mli | 4 ++-- ide/config_lexer.mli | 4 ++-- ide/config_lexer.mll | 4 ++-- ide/coq.ml | 4 ++-- ide/coq.mli | 4 ++-- ide/coqOps.ml | 4 ++-- ide/coqOps.mli | 4 ++-- ide/coq_commands.ml | 4 ++-- ide/coq_commands.mli | 4 ++-- ide/coq_lex.mli | 4 ++-- ide/coq_lex.mll | 4 ++-- ide/coqide.ml | 4 ++-- ide/coqide.mli | 4 ++-- ide/coqide_QUARTZ.ml.in | 4 ++-- ide/coqide_WIN32.ml.in | 4 ++-- ide/coqide_X11.ml.in | 4 ++-- ide/coqide_main.ml | 4 ++-- ide/coqide_main.mli | 4 ++-- ide/coqide_os_specific.mli | 4 ++-- ide/coqide_ui.mli | 4 ++-- ide/document.ml | 4 ++-- ide/document.mli | 4 ++-- ide/fake_ide.ml | 4 ++-- ide/fileOps.ml | 4 ++-- ide/fileOps.mli | 4 ++-- ide/gtk_parsing.ml | 4 ++-- ide/gtk_parsing.mli | 4 ++-- ide/idetop.ml | 4 ++-- ide/ideutils.ml | 4 ++-- ide/ideutils.mli | 4 ++-- ide/macos_prehook.mli | 4 ++-- ide/microPG.ml | 4 ++-- ide/microPG.mli | 4 ++-- ide/minilib.ml | 4 ++-- ide/minilib.mli | 4 ++-- ide/preferences.ml | 4 ++-- ide/preferences.mli | 4 ++-- ide/protocol/interface.ml | 4 ++-- ide/protocol/richpp.ml | 4 ++-- ide/protocol/richpp.mli | 4 ++-- ide/protocol/serialize.ml | 4 ++-- ide/protocol/serialize.mli | 4 ++-- ide/protocol/xml_printer.ml | 4 ++-- ide/protocol/xml_printer.mli | 4 ++-- ide/protocol/xmlprotocol.ml | 4 ++-- ide/protocol/xmlprotocol.mli | 4 ++-- ide/sentence.ml | 4 ++-- ide/sentence.mli | 4 ++-- ide/session.ml | 4 ++-- ide/session.mli | 4 ++-- ide/tags.ml | 4 ++-- ide/tags.mli | 4 ++-- ide/unicode_bindings.ml | 4 ++-- ide/unicode_bindings.mli | 4 ++-- ide/utf8_convert.mli | 4 ++-- ide/utf8_convert.mll | 4 ++-- ide/wg_Command.ml | 4 ++-- ide/wg_Command.mli | 4 ++-- ide/wg_Completion.ml | 4 ++-- ide/wg_Completion.mli | 4 ++-- ide/wg_Detachable.ml | 4 ++-- ide/wg_Detachable.mli | 4 ++-- ide/wg_Find.ml | 4 ++-- ide/wg_Find.mli | 4 ++-- ide/wg_MessageView.ml | 4 ++-- ide/wg_MessageView.mli | 4 ++-- ide/wg_Notebook.ml | 4 ++-- ide/wg_Notebook.mli | 4 ++-- ide/wg_ProofView.ml | 4 ++-- ide/wg_ProofView.mli | 4 ++-- ide/wg_RoutedMessageViews.ml | 4 ++-- ide/wg_RoutedMessageViews.mli | 4 ++-- ide/wg_ScriptView.ml | 4 ++-- ide/wg_ScriptView.mli | 4 ++-- ide/wg_Segment.ml | 4 ++-- ide/wg_Segment.mli | 4 ++-- interp/constrexpr.ml | 4 ++-- interp/constrexpr_ops.ml | 4 ++-- interp/constrexpr_ops.mli | 4 ++-- interp/constrextern.ml | 4 ++-- interp/constrextern.mli | 4 ++-- interp/constrintern.ml | 4 ++-- interp/constrintern.mli | 4 ++-- interp/decls.ml | 4 ++-- interp/decls.mli | 4 ++-- interp/deprecation.ml | 4 ++-- interp/deprecation.mli | 4 ++-- interp/dumpglob.ml | 4 ++-- interp/dumpglob.mli | 4 ++-- interp/genintern.ml | 4 ++-- interp/genintern.mli | 4 ++-- interp/impargs.ml | 4 ++-- interp/impargs.mli | 4 ++-- interp/implicit_quantifiers.ml | 4 ++-- interp/implicit_quantifiers.mli | 4 ++-- interp/modintern.ml | 4 ++-- interp/modintern.mli | 4 ++-- interp/notation.ml | 4 ++-- interp/notation.mli | 4 ++-- interp/notation_ops.ml | 4 ++-- interp/notation_ops.mli | 4 ++-- interp/notation_term.ml | 4 ++-- interp/numTok.ml | 10 ++++++++++ interp/numTok.mli | 10 ++++++++++ interp/reserve.ml | 4 ++-- interp/reserve.mli | 4 ++-- interp/smartlocate.ml | 4 ++-- interp/smartlocate.mli | 4 ++-- interp/stdarg.ml | 4 ++-- interp/stdarg.mli | 4 ++-- interp/syntax_def.ml | 4 ++-- interp/syntax_def.mli | 4 ++-- kernel/byterun/coq_float64.h | 10 ++++++++++ kernel/byterun/coq_uint63_emul.h | 10 ++++++++++ kernel/byterun/coq_uint63_native.h | 10 ++++++++++ kernel/cClosure.ml | 4 ++-- kernel/cClosure.mli | 4 ++-- kernel/cPrimitives.ml | 4 ++-- kernel/cPrimitives.mli | 4 ++-- kernel/cbytecodes.ml | 4 ++-- kernel/cbytecodes.mli | 4 ++-- kernel/cbytegen.ml | 4 ++-- kernel/cbytegen.mli | 4 ++-- kernel/cemitcodes.ml | 4 ++-- kernel/cemitcodes.mli | 4 ++-- kernel/constr.ml | 4 ++-- kernel/constr.mli | 4 ++-- kernel/context.ml | 4 ++-- kernel/context.mli | 4 ++-- kernel/conv_oracle.ml | 4 ++-- kernel/conv_oracle.mli | 4 ++-- kernel/cooking.ml | 4 ++-- kernel/cooking.mli | 4 ++-- kernel/csymtable.ml | 4 ++-- kernel/csymtable.mli | 4 ++-- kernel/declarations.ml | 4 ++-- kernel/declareops.ml | 4 ++-- kernel/declareops.mli | 4 ++-- kernel/entries.ml | 4 ++-- kernel/environ.ml | 4 ++-- kernel/environ.mli | 4 ++-- kernel/esubst.ml | 4 ++-- kernel/esubst.mli | 4 ++-- kernel/evar.ml | 4 ++-- kernel/evar.mli | 4 ++-- kernel/float64.ml | 4 ++-- kernel/float64.mli | 4 ++-- kernel/genOpcodeFiles.ml | 4 ++-- kernel/indTyping.ml | 4 ++-- kernel/indTyping.mli | 4 ++-- kernel/indtypes.ml | 4 ++-- kernel/indtypes.mli | 4 ++-- kernel/inductive.ml | 4 ++-- kernel/inductive.mli | 4 ++-- kernel/inferCumulativity.ml | 4 ++-- kernel/inferCumulativity.mli | 4 ++-- kernel/mod_subst.ml | 4 ++-- kernel/mod_subst.mli | 4 ++-- kernel/mod_typing.ml | 4 ++-- kernel/mod_typing.mli | 4 ++-- kernel/modops.ml | 4 ++-- kernel/modops.mli | 4 ++-- kernel/names.ml | 4 ++-- kernel/names.mli | 4 ++-- kernel/nativecode.ml | 4 ++-- kernel/nativecode.mli | 4 ++-- kernel/nativeconv.ml | 4 ++-- kernel/nativeconv.mli | 4 ++-- kernel/nativelambda.ml | 4 ++-- kernel/nativelambda.mli | 4 ++-- kernel/nativelib.ml | 4 ++-- kernel/nativelib.mli | 4 ++-- kernel/nativelibrary.ml | 4 ++-- kernel/nativelibrary.mli | 4 ++-- kernel/nativevalues.ml | 4 ++-- kernel/nativevalues.mli | 4 ++-- kernel/opaqueproof.ml | 4 ++-- kernel/opaqueproof.mli | 4 ++-- kernel/reduction.ml | 4 ++-- kernel/reduction.mli | 4 ++-- kernel/retroknowledge.ml | 4 ++-- kernel/retroknowledge.mli | 4 ++-- kernel/retypeops.ml | 4 ++-- kernel/retypeops.mli | 4 ++-- kernel/safe_typing.ml | 4 ++-- kernel/safe_typing.mli | 4 ++-- kernel/section.ml | 4 ++-- kernel/section.mli | 4 ++-- kernel/sorts.ml | 4 ++-- kernel/sorts.mli | 4 ++-- kernel/subtyping.ml | 4 ++-- kernel/subtyping.mli | 4 ++-- kernel/term.ml | 4 ++-- kernel/term.mli | 4 ++-- kernel/term_typing.ml | 4 ++-- kernel/term_typing.mli | 4 ++-- kernel/transparentState.ml | 4 ++-- kernel/transparentState.mli | 4 ++-- kernel/type_errors.ml | 4 ++-- kernel/type_errors.mli | 4 ++-- kernel/typeops.ml | 4 ++-- kernel/typeops.mli | 4 ++-- kernel/uGraph.ml | 4 ++-- kernel/uGraph.mli | 4 ++-- kernel/uint63.mli | 4 ++-- kernel/uint63_31.ml | 4 ++-- kernel/uint63_63.ml | 4 ++-- kernel/univ.ml | 4 ++-- kernel/univ.mli | 4 ++-- kernel/vars.ml | 4 ++-- kernel/vars.mli | 4 ++-- kernel/vconv.mli | 4 ++-- kernel/vm.ml | 4 ++-- kernel/vm.mli | 4 ++-- kernel/vmvalues.ml | 4 ++-- kernel/vmvalues.mli | 4 ++-- lib/acyclicGraph.ml | 4 ++-- lib/acyclicGraph.mli | 4 ++-- lib/aux_file.ml | 4 ++-- lib/aux_file.mli | 4 ++-- lib/cAst.ml | 4 ++-- lib/cAst.mli | 4 ++-- lib/cErrors.ml | 4 ++-- lib/cErrors.mli | 4 ++-- lib/cProfile.ml | 4 ++-- lib/cProfile.mli | 4 ++-- lib/cWarnings.ml | 4 ++-- lib/cWarnings.mli | 4 ++-- lib/control.ml | 4 ++-- lib/control.mli | 4 ++-- lib/coqProject_file.ml | 4 ++-- lib/coqProject_file.mli | 4 ++-- lib/dAst.ml | 4 ++-- lib/dAst.mli | 4 ++-- lib/envars.ml | 4 ++-- lib/envars.mli | 4 ++-- lib/explore.ml | 4 ++-- lib/explore.mli | 4 ++-- lib/feedback.ml | 4 ++-- lib/feedback.mli | 4 ++-- lib/flags.ml | 4 ++-- lib/flags.mli | 4 ++-- lib/future.ml | 4 ++-- lib/future.mli | 4 ++-- lib/genarg.ml | 4 ++-- lib/genarg.mli | 4 ++-- lib/hook.ml | 4 ++-- lib/hook.mli | 4 ++-- lib/loc.ml | 4 ++-- lib/loc.mli | 4 ++-- lib/pp.ml | 4 ++-- lib/pp.mli | 4 ++-- lib/pp_diff.ml | 4 ++-- lib/pp_diff.mli | 4 ++-- lib/remoteCounter.ml | 4 ++-- lib/remoteCounter.mli | 4 ++-- lib/rtree.ml | 4 ++-- lib/rtree.mli | 4 ++-- lib/spawn.ml | 4 ++-- lib/spawn.mli | 4 ++-- lib/stateid.ml | 4 ++-- lib/stateid.mli | 4 ++-- lib/system.ml | 4 ++-- lib/system.mli | 4 ++-- lib/util.ml | 4 ++-- lib/util.mli | 4 ++-- lib/xml_datatype.mli | 4 ++-- library/coqlib.ml | 4 ++-- library/coqlib.mli | 4 ++-- library/global.ml | 4 ++-- library/global.mli | 4 ++-- library/globnames.ml | 4 ++-- library/globnames.mli | 4 ++-- library/goptions.ml | 4 ++-- library/goptions.mli | 4 ++-- library/lib.ml | 4 ++-- library/lib.mli | 4 ++-- library/libnames.ml | 4 ++-- library/libnames.mli | 4 ++-- library/libobject.ml | 4 ++-- library/libobject.mli | 4 ++-- library/nametab.ml | 4 ++-- library/nametab.mli | 4 ++-- library/states.ml | 4 ++-- library/states.mli | 4 ++-- library/summary.ml | 4 ++-- library/summary.mli | 4 ++-- parsing/cLexer.ml | 4 ++-- parsing/cLexer.mli | 4 ++-- parsing/extend.ml | 4 ++-- parsing/g_constr.mlg | 4 ++-- parsing/g_prim.mlg | 4 ++-- parsing/notation_gram.ml | 4 ++-- parsing/notgram_ops.ml | 4 ++-- parsing/notgram_ops.mli | 4 ++-- parsing/pcoq.ml | 4 ++-- parsing/pcoq.mli | 4 ++-- parsing/ppextend.ml | 4 ++-- parsing/ppextend.mli | 4 ++-- parsing/tok.ml | 4 ++-- parsing/tok.mli | 4 ++-- plugins/btauto/g_btauto.mlg | 4 ++-- plugins/btauto/refl_btauto.ml | 4 ++-- plugins/btauto/refl_btauto.mli | 4 ++-- plugins/cc/ccalgo.ml | 4 ++-- plugins/cc/ccalgo.mli | 4 ++-- plugins/cc/ccproof.ml | 4 ++-- plugins/cc/ccproof.mli | 4 ++-- plugins/cc/cctac.ml | 4 ++-- plugins/cc/cctac.mli | 4 ++-- plugins/cc/g_congruence.mlg | 4 ++-- plugins/derive/derive.ml | 4 ++-- plugins/derive/derive.mli | 4 ++-- plugins/derive/g_derive.mlg | 4 ++-- plugins/extraction/big.ml | 4 ++-- plugins/extraction/common.ml | 4 ++-- plugins/extraction/common.mli | 4 ++-- plugins/extraction/extract_env.ml | 4 ++-- plugins/extraction/extract_env.mli | 4 ++-- plugins/extraction/extraction.ml | 4 ++-- plugins/extraction/extraction.mli | 4 ++-- plugins/extraction/g_extraction.mlg | 4 ++-- plugins/extraction/haskell.ml | 4 ++-- plugins/extraction/haskell.mli | 4 ++-- plugins/extraction/miniml.ml | 4 ++-- plugins/extraction/miniml.mli | 4 ++-- plugins/extraction/mlutil.ml | 4 ++-- plugins/extraction/mlutil.mli | 4 ++-- plugins/extraction/modutil.ml | 4 ++-- plugins/extraction/modutil.mli | 4 ++-- plugins/extraction/ocaml.ml | 4 ++-- plugins/extraction/ocaml.mli | 4 ++-- plugins/extraction/scheme.ml | 4 ++-- plugins/extraction/scheme.mli | 4 ++-- plugins/extraction/table.ml | 4 ++-- plugins/extraction/table.mli | 4 ++-- plugins/firstorder/formula.ml | 4 ++-- plugins/firstorder/formula.mli | 4 ++-- plugins/firstorder/g_ground.mlg | 4 ++-- plugins/firstorder/ground.ml | 4 ++-- plugins/firstorder/ground.mli | 4 ++-- plugins/firstorder/instances.ml | 4 ++-- plugins/firstorder/instances.mli | 4 ++-- plugins/firstorder/rules.ml | 4 ++-- plugins/firstorder/rules.mli | 4 ++-- plugins/firstorder/sequent.ml | 4 ++-- plugins/firstorder/sequent.mli | 4 ++-- plugins/firstorder/unify.ml | 4 ++-- plugins/firstorder/unify.mli | 4 ++-- plugins/funind/functional_principles_types.ml | 4 ++-- plugins/funind/functional_principles_types.mli | 4 ++-- plugins/funind/g_indfun.mlg | 4 ++-- plugins/funind/gen_principle.ml | 4 ++-- plugins/funind/gen_principle.mli | 4 ++-- plugins/funind/glob_termops.ml | 4 ++-- plugins/funind/glob_termops.mli | 4 ++-- plugins/funind/indfun.ml | 4 ++-- plugins/funind/indfun.mli | 4 ++-- plugins/funind/invfun.ml | 4 ++-- plugins/funind/invfun.mli | 4 ++-- plugins/funind/recdef.ml | 4 ++-- plugins/ltac/coretactics.mlg | 4 ++-- plugins/ltac/evar_tactics.ml | 4 ++-- plugins/ltac/evar_tactics.mli | 4 ++-- plugins/ltac/extraargs.mlg | 4 ++-- plugins/ltac/extraargs.mli | 4 ++-- plugins/ltac/extratactics.mlg | 4 ++-- plugins/ltac/extratactics.mli | 4 ++-- plugins/ltac/g_auto.mlg | 4 ++-- plugins/ltac/g_class.mlg | 4 ++-- plugins/ltac/g_eqdecide.mlg | 4 ++-- plugins/ltac/g_ltac.mlg | 4 ++-- plugins/ltac/g_obligations.mlg | 4 ++-- plugins/ltac/g_rewrite.mlg | 4 ++-- plugins/ltac/g_tactic.mlg | 4 ++-- plugins/ltac/pltac.ml | 4 ++-- plugins/ltac/pltac.mli | 4 ++-- plugins/ltac/pptactic.ml | 4 ++-- plugins/ltac/pptactic.mli | 4 ++-- plugins/ltac/profile_ltac.ml | 4 ++-- plugins/ltac/profile_ltac.mli | 4 ++-- plugins/ltac/profile_ltac_tactics.mlg | 4 ++-- plugins/ltac/rewrite.ml | 4 ++-- plugins/ltac/rewrite.mli | 4 ++-- plugins/ltac/tacarg.ml | 4 ++-- plugins/ltac/tacarg.mli | 4 ++-- plugins/ltac/taccoerce.ml | 4 ++-- plugins/ltac/taccoerce.mli | 4 ++-- plugins/ltac/tacentries.ml | 4 ++-- plugins/ltac/tacentries.mli | 4 ++-- plugins/ltac/tacenv.ml | 4 ++-- plugins/ltac/tacenv.mli | 4 ++-- plugins/ltac/tacexpr.ml | 4 ++-- plugins/ltac/tacexpr.mli | 4 ++-- plugins/ltac/tacintern.ml | 4 ++-- plugins/ltac/tacintern.mli | 4 ++-- plugins/ltac/tacinterp.ml | 4 ++-- plugins/ltac/tacinterp.mli | 4 ++-- plugins/ltac/tacsubst.ml | 4 ++-- plugins/ltac/tacsubst.mli | 4 ++-- plugins/ltac/tactic_debug.ml | 4 ++-- plugins/ltac/tactic_debug.mli | 4 ++-- plugins/ltac/tactic_matching.ml | 4 ++-- plugins/ltac/tactic_matching.mli | 4 ++-- plugins/ltac/tactic_option.ml | 4 ++-- plugins/ltac/tactic_option.mli | 4 ++-- plugins/ltac/tauto.ml | 4 ++-- plugins/micromega/certificate.ml | 4 ++-- plugins/micromega/certificate.mli | 4 ++-- plugins/micromega/coq_micromega.ml | 4 ++-- plugins/micromega/coq_micromega.mli | 4 ++-- plugins/micromega/csdpcert.ml | 4 ++-- plugins/micromega/csdpcert.mli | 4 ++-- plugins/micromega/g_micromega.mlg | 4 ++-- plugins/micromega/g_micromega.mli | 4 ++-- plugins/micromega/g_zify.mlg | 4 ++-- plugins/micromega/itv.ml | 4 ++-- plugins/micromega/itv.mli | 4 ++-- plugins/micromega/mfourier.ml | 4 ++-- plugins/micromega/mfourier.mli | 4 ++-- plugins/micromega/mutils.ml | 4 ++-- plugins/micromega/mutils.mli | 4 ++-- plugins/micromega/numCompat.ml | 4 ++-- plugins/micromega/numCompat.mli | 4 ++-- plugins/micromega/persistent_cache.ml | 4 ++-- plugins/micromega/persistent_cache.mli | 4 ++-- plugins/micromega/polynomial.ml | 4 ++-- plugins/micromega/polynomial.mli | 4 ++-- plugins/micromega/simplex.ml | 4 ++-- plugins/micromega/simplex.mli | 4 ++-- plugins/micromega/sos.mli | 4 ++-- plugins/micromega/sos_lib.mli | 4 ++-- plugins/micromega/sos_types.ml | 4 ++-- plugins/micromega/sos_types.mli | 4 ++-- plugins/micromega/vect.ml | 4 ++-- plugins/micromega/vect.mli | 4 ++-- plugins/micromega/zify.ml | 4 ++-- plugins/micromega/zify.mli | 4 ++-- plugins/nsatz/g_nsatz.mlg | 4 ++-- plugins/nsatz/ideal.ml | 4 ++-- plugins/nsatz/ideal.mli | 4 ++-- plugins/nsatz/nsatz.ml | 4 ++-- plugins/nsatz/nsatz.mli | 4 ++-- plugins/nsatz/polynom.ml | 4 ++-- plugins/nsatz/polynom.mli | 4 ++-- plugins/omega/coq_omega.ml | 4 ++-- plugins/omega/coq_omega.mli | 4 ++-- plugins/omega/g_omega.mlg | 4 ++-- plugins/omega/omega.ml | 4 ++-- plugins/rtauto/g_rtauto.mlg | 4 ++-- plugins/rtauto/proof_search.ml | 4 ++-- plugins/rtauto/proof_search.mli | 4 ++-- plugins/rtauto/refl_tauto.ml | 4 ++-- plugins/rtauto/refl_tauto.mli | 4 ++-- plugins/setoid_ring/g_newring.mlg | 4 ++-- plugins/setoid_ring/newring.ml | 4 ++-- plugins/setoid_ring/newring.mli | 4 ++-- plugins/setoid_ring/newring_ast.ml | 4 ++-- plugins/setoid_ring/newring_ast.mli | 4 ++-- plugins/ssr/ssrast.mli | 4 ++-- plugins/ssr/ssrbwd.ml | 4 ++-- plugins/ssr/ssrbwd.mli | 4 ++-- plugins/ssr/ssrcommon.ml | 4 ++-- plugins/ssr/ssrcommon.mli | 4 ++-- plugins/ssr/ssrelim.ml | 4 ++-- plugins/ssr/ssrelim.mli | 4 ++-- plugins/ssr/ssrequality.ml | 4 ++-- plugins/ssr/ssrequality.mli | 4 ++-- plugins/ssr/ssrfwd.ml | 4 ++-- plugins/ssr/ssrfwd.mli | 4 ++-- plugins/ssr/ssripats.ml | 4 ++-- plugins/ssr/ssripats.mli | 4 ++-- plugins/ssr/ssrparser.mlg | 4 ++-- plugins/ssr/ssrparser.mli | 4 ++-- plugins/ssr/ssrprinters.ml | 4 ++-- plugins/ssr/ssrprinters.mli | 4 ++-- plugins/ssr/ssrtacticals.ml | 4 ++-- plugins/ssr/ssrtacticals.mli | 4 ++-- plugins/ssr/ssrvernac.mlg | 4 ++-- plugins/ssr/ssrvernac.mli | 4 ++-- plugins/ssr/ssrview.ml | 4 ++-- plugins/ssr/ssrview.mli | 4 ++-- plugins/ssrmatching/g_ssrmatching.mlg | 4 ++-- plugins/ssrmatching/g_ssrmatching.mli | 4 ++-- plugins/ssrmatching/ssrmatching.ml | 4 ++-- plugins/ssrmatching/ssrmatching.mli | 4 ++-- plugins/syntax/float_syntax.ml | 10 ++++++---- plugins/syntax/g_numeral.mlg | 4 ++-- plugins/syntax/g_string.mlg | 4 ++-- plugins/syntax/int63_syntax.ml | 4 ++-- plugins/syntax/numeral.ml | 4 ++-- plugins/syntax/numeral.mli | 4 ++-- plugins/syntax/r_syntax.ml | 4 ++-- plugins/syntax/r_syntax.mli | 4 ++-- plugins/syntax/string_notation.ml | 4 ++-- plugins/syntax/string_notation.mli | 4 ++-- pretyping/arguments_renaming.ml | 4 ++-- pretyping/arguments_renaming.mli | 4 ++-- pretyping/cases.ml | 4 ++-- pretyping/cases.mli | 4 ++-- pretyping/cbv.ml | 4 ++-- pretyping/cbv.mli | 4 ++-- pretyping/coercion.ml | 4 ++-- pretyping/coercion.mli | 4 ++-- pretyping/coercionops.ml | 4 ++-- pretyping/coercionops.mli | 4 ++-- pretyping/constr_matching.ml | 4 ++-- pretyping/constr_matching.mli | 4 ++-- pretyping/detyping.ml | 4 ++-- pretyping/detyping.mli | 4 ++-- pretyping/evarconv.ml | 4 ++-- pretyping/evarconv.mli | 4 ++-- pretyping/evardefine.ml | 4 ++-- pretyping/evardefine.mli | 4 ++-- pretyping/evarsolve.ml | 4 ++-- pretyping/evarsolve.mli | 4 ++-- pretyping/find_subterm.ml | 4 ++-- pretyping/find_subterm.mli | 4 ++-- pretyping/geninterp.ml | 4 ++-- pretyping/geninterp.mli | 4 ++-- pretyping/globEnv.ml | 4 ++-- pretyping/globEnv.mli | 4 ++-- pretyping/glob_ops.ml | 4 ++-- pretyping/glob_ops.mli | 4 ++-- pretyping/glob_term.ml | 4 ++-- pretyping/heads.ml | 4 ++-- pretyping/heads.mli | 4 ++-- pretyping/indrec.ml | 4 ++-- pretyping/indrec.mli | 4 ++-- pretyping/inductiveops.ml | 4 ++-- pretyping/inductiveops.mli | 4 ++-- pretyping/keys.ml | 4 ++-- pretyping/keys.mli | 4 ++-- pretyping/locus.ml | 4 ++-- pretyping/locusops.ml | 4 ++-- pretyping/locusops.mli | 4 ++-- pretyping/nativenorm.ml | 4 ++-- pretyping/nativenorm.mli | 4 ++-- pretyping/pattern.ml | 4 ++-- pretyping/patternops.ml | 4 ++-- pretyping/patternops.mli | 4 ++-- pretyping/pretype_errors.ml | 4 ++-- pretyping/pretype_errors.mli | 4 ++-- pretyping/pretyping.ml | 4 ++-- pretyping/pretyping.mli | 4 ++-- pretyping/program.ml | 4 ++-- pretyping/program.mli | 4 ++-- pretyping/recordops.ml | 4 ++-- pretyping/recordops.mli | 4 ++-- pretyping/reductionops.ml | 4 ++-- pretyping/reductionops.mli | 4 ++-- pretyping/retyping.ml | 4 ++-- pretyping/retyping.mli | 4 ++-- pretyping/tacred.ml | 4 ++-- pretyping/tacred.mli | 4 ++-- pretyping/typeclasses.ml | 4 ++-- pretyping/typeclasses.mli | 4 ++-- pretyping/typeclasses_errors.ml | 4 ++-- pretyping/typeclasses_errors.mli | 4 ++-- pretyping/typing.ml | 4 ++-- pretyping/typing.mli | 4 ++-- pretyping/unification.ml | 4 ++-- pretyping/unification.mli | 4 ++-- pretyping/vnorm.ml | 4 ++-- pretyping/vnorm.mli | 4 ++-- printing/genprint.ml | 4 ++-- printing/genprint.mli | 4 ++-- printing/ppconstr.ml | 4 ++-- printing/ppconstr.mli | 4 ++-- printing/pputils.ml | 4 ++-- printing/pputils.mli | 4 ++-- printing/printer.ml | 4 ++-- printing/printer.mli | 4 ++-- printing/printmod.ml | 4 ++-- printing/printmod.mli | 4 ++-- printing/proof_diffs.ml | 4 ++-- printing/proof_diffs.mli | 4 ++-- proofs/clenv.ml | 4 ++-- proofs/clenv.mli | 4 ++-- proofs/clenvtac.ml | 4 ++-- proofs/clenvtac.mli | 4 ++-- proofs/evar_refiner.ml | 4 ++-- proofs/evar_refiner.mli | 4 ++-- proofs/goal.ml | 4 ++-- proofs/goal.mli | 4 ++-- proofs/goal_select.ml | 4 ++-- proofs/goal_select.mli | 4 ++-- proofs/logic.ml | 4 ++-- proofs/logic.mli | 4 ++-- proofs/miscprint.ml | 4 ++-- proofs/miscprint.mli | 4 ++-- proofs/proof.ml | 4 ++-- proofs/proof.mli | 4 ++-- proofs/proof_bullet.ml | 4 ++-- proofs/proof_bullet.mli | 4 ++-- proofs/refine.ml | 4 ++-- proofs/refine.mli | 4 ++-- proofs/refiner.ml | 4 ++-- proofs/refiner.mli | 4 ++-- proofs/tacmach.ml | 4 ++-- proofs/tacmach.mli | 4 ++-- proofs/tactypes.ml | 4 ++-- stm/asyncTaskQueue.ml | 4 ++-- stm/asyncTaskQueue.mli | 4 ++-- stm/coqworkmgrApi.ml | 4 ++-- stm/coqworkmgrApi.mli | 4 ++-- stm/dag.ml | 4 ++-- stm/dag.mli | 4 ++-- stm/proofBlockDelimiter.ml | 4 ++-- stm/proofBlockDelimiter.mli | 4 ++-- stm/spawned.ml | 4 ++-- stm/spawned.mli | 4 ++-- stm/stm.ml | 4 ++-- stm/stm.mli | 4 ++-- stm/tQueue.ml | 4 ++-- stm/tQueue.mli | 4 ++-- stm/vcs.ml | 4 ++-- stm/vcs.mli | 4 ++-- stm/vernac_classifier.ml | 4 ++-- stm/vernac_classifier.mli | 4 ++-- stm/vio_checking.ml | 4 ++-- stm/vio_checking.mli | 4 ++-- stm/workerPool.ml | 4 ++-- stm/workerPool.mli | 4 ++-- tactics/abstract.ml | 4 ++-- tactics/abstract.mli | 4 ++-- tactics/auto.ml | 4 ++-- tactics/auto.mli | 4 ++-- tactics/autorewrite.ml | 4 ++-- tactics/autorewrite.mli | 4 ++-- tactics/btermdn.ml | 4 ++-- tactics/btermdn.mli | 4 ++-- tactics/class_tactics.ml | 4 ++-- tactics/class_tactics.mli | 4 ++-- tactics/contradiction.ml | 4 ++-- tactics/contradiction.mli | 4 ++-- tactics/declare.ml | 4 ++-- tactics/declare.mli | 4 ++-- tactics/declareScheme.ml | 4 ++-- tactics/declareScheme.mli | 4 ++-- tactics/dnet.ml | 4 ++-- tactics/dnet.mli | 4 ++-- tactics/eauto.ml | 4 ++-- tactics/eauto.mli | 4 ++-- tactics/elim.ml | 4 ++-- tactics/elim.mli | 4 ++-- tactics/elimschemes.ml | 4 ++-- tactics/elimschemes.mli | 4 ++-- tactics/eqdecide.ml | 4 ++-- tactics/eqdecide.mli | 4 ++-- tactics/eqschemes.ml | 4 ++-- tactics/eqschemes.mli | 4 ++-- tactics/equality.ml | 4 ++-- tactics/equality.mli | 4 ++-- tactics/genredexpr.ml | 4 ++-- tactics/hints.ml | 4 ++-- tactics/hints.mli | 4 ++-- tactics/hipattern.ml | 4 ++-- tactics/hipattern.mli | 4 ++-- tactics/ind_tables.ml | 4 ++-- tactics/ind_tables.mli | 4 ++-- tactics/inv.ml | 4 ++-- tactics/inv.mli | 4 ++-- tactics/leminv.ml | 4 ++-- tactics/leminv.mli | 4 ++-- tactics/pfedit.ml | 4 ++-- tactics/pfedit.mli | 4 ++-- tactics/proof_global.ml | 4 ++-- tactics/proof_global.mli | 4 ++-- tactics/redexpr.ml | 4 ++-- tactics/redexpr.mli | 4 ++-- tactics/redops.ml | 4 ++-- tactics/redops.mli | 4 ++-- tactics/tacticals.ml | 4 ++-- tactics/tacticals.mli | 4 ++-- tactics/tactics.ml | 4 ++-- tactics/tactics.mli | 4 ++-- tactics/term_dnet.ml | 4 ++-- tactics/term_dnet.mli | 4 ++-- test-suite/Makefile | 4 ++-- test-suite/failure/Tauto.v | 4 ++-- test-suite/failure/clash_cons.v | 4 ++-- test-suite/failure/fixpoint1.v | 4 ++-- test-suite/failure/guard.v | 4 ++-- test-suite/failure/illtype1.v | 4 ++-- test-suite/failure/positivity.v | 4 ++-- test-suite/failure/redef.v | 4 ++-- test-suite/failure/search.v | 4 ++-- test-suite/ideal-features/Apply.v | 4 ++-- test-suite/output/FloatExtraction.v | 4 ++-- test-suite/output/MExtraction.v | 4 ++-- test-suite/output/ssr_explain_match.v | 4 ++-- test-suite/prerequisite/ssr_mini_mathcomp.v | 4 ++-- test-suite/prerequisite/ssr_ssrsyntax1.v | 4 ++-- test-suite/ssr/absevarprop.v | 4 ++-- test-suite/ssr/abstract_var2.v | 4 ++-- test-suite/ssr/binders.v | 4 ++-- test-suite/ssr/binders_of.v | 4 ++-- test-suite/ssr/caseview.v | 4 ++-- test-suite/ssr/congr.v | 4 ++-- test-suite/ssr/deferclear.v | 4 ++-- test-suite/ssr/dependent_type_err.v | 4 ++-- test-suite/ssr/derive_inversion.v | 4 ++-- test-suite/ssr/elim.v | 4 ++-- test-suite/ssr/elim2.v | 4 ++-- test-suite/ssr/elim_pattern.v | 4 ++-- test-suite/ssr/first_n.v | 4 ++-- test-suite/ssr/gen_have.v | 4 ++-- test-suite/ssr/gen_pattern.v | 4 ++-- test-suite/ssr/have_TC.v | 4 ++-- test-suite/ssr/have_transp.v | 4 ++-- test-suite/ssr/have_view_idiom.v | 4 ++-- test-suite/ssr/havesuff.v | 4 ++-- test-suite/ssr/if_isnt.v | 4 ++-- test-suite/ssr/intro_beta.v | 4 ++-- test-suite/ssr/intro_noop.v | 4 ++-- test-suite/ssr/ipatalternation.v | 4 ++-- test-suite/ssr/ltac_have.v | 4 ++-- test-suite/ssr/ltac_in.v | 4 ++-- test-suite/ssr/move_after.v | 4 ++-- test-suite/ssr/multiview.v | 4 ++-- test-suite/ssr/occarrow.v | 4 ++-- test-suite/ssr/patnoX.v | 4 ++-- test-suite/ssr/pattern.v | 4 ++-- test-suite/ssr/primproj.v | 4 ++-- test-suite/ssr/rewpatterns.v | 4 ++-- test-suite/ssr/set_lamda.v | 4 ++-- test-suite/ssr/set_pattern.v | 4 ++-- test-suite/ssr/ssrsyntax2.v | 4 ++-- test-suite/ssr/tc.v | 4 ++-- test-suite/ssr/typeof.v | 4 ++-- test-suite/ssr/unfold_Opaque.v | 4 ++-- test-suite/ssr/unkeyed.v | 4 ++-- test-suite/ssr/view_case.v | 4 ++-- test-suite/ssr/wlog_suff.v | 4 ++-- test-suite/ssr/wlogletin.v | 4 ++-- test-suite/ssr/wlong_intro.v | 4 ++-- test-suite/success/Check.v | 4 ++-- test-suite/success/Field.v | 4 ++-- test-suite/success/Tauto.v | 4 ++-- test-suite/success/TestRefine.v | 4 ++-- test-suite/success/eauto.v | 4 ++-- test-suite/success/eqdecide.v | 4 ++-- test-suite/success/extraction.v | 4 ++-- test-suite/success/inds_type_sec.v | 4 ++-- test-suite/success/induct.v | 4 ++-- test-suite/success/mutual_ind.v | 4 ++-- test-suite/success/unfold.v | 4 ++-- test-suite/typeclasses/NewSetoid.v | 4 ++-- theories/Arith/Arith.v | 4 ++-- theories/Arith/Arith_base.v | 4 ++-- theories/Arith/Between.v | 4 ++-- theories/Arith/Bool_nat.v | 4 ++-- theories/Arith/Compare.v | 4 ++-- theories/Arith/Compare_dec.v | 4 ++-- theories/Arith/Div2.v | 4 ++-- theories/Arith/EqNat.v | 4 ++-- theories/Arith/Euclid.v | 4 ++-- theories/Arith/Even.v | 4 ++-- theories/Arith/Factorial.v | 4 ++-- theories/Arith/Gt.v | 4 ++-- theories/Arith/Le.v | 4 ++-- theories/Arith/Lt.v | 4 ++-- theories/Arith/Max.v | 4 ++-- theories/Arith/Min.v | 4 ++-- theories/Arith/Minus.v | 4 ++-- theories/Arith/Mult.v | 4 ++-- theories/Arith/PeanoNat.v | 4 ++-- theories/Arith/Peano_dec.v | 4 ++-- theories/Arith/Plus.v | 4 ++-- theories/Arith/Wf_nat.v | 4 ++-- theories/Bool/Bool.v | 4 ++-- theories/Bool/BoolEq.v | 4 ++-- theories/Bool/Bvector.v | 4 ++-- theories/Bool/DecBool.v | 4 ++-- theories/Bool/IfProp.v | 4 ++-- theories/Bool/Sumbool.v | 4 ++-- theories/Bool/Zerob.v | 4 ++-- theories/Classes/CEquivalence.v | 4 ++-- theories/Classes/CMorphisms.v | 4 ++-- theories/Classes/CRelationClasses.v | 4 ++-- theories/Classes/DecidableClass.v | 4 ++-- theories/Classes/EquivDec.v | 4 ++-- theories/Classes/Equivalence.v | 4 ++-- theories/Classes/Init.v | 4 ++-- theories/Classes/Morphisms.v | 4 ++-- theories/Classes/Morphisms_Prop.v | 4 ++-- theories/Classes/Morphisms_Relations.v | 4 ++-- theories/Classes/RelationClasses.v | 4 ++-- theories/Classes/RelationPairs.v | 4 ++-- theories/Classes/SetoidClass.v | 4 ++-- theories/Classes/SetoidDec.v | 4 ++-- theories/Classes/SetoidTactics.v | 4 ++-- theories/Compat/AdmitAxiom.v | 4 ++-- theories/Compat/Coq810.v | 4 ++-- theories/Compat/Coq811.v | 4 ++-- theories/Compat/Coq812.v | 4 ++-- theories/FSets/FMapAVL.v | 4 ++-- theories/FSets/FMapFacts.v | 4 ++-- theories/FSets/FMapFullAVL.v | 4 ++-- theories/FSets/FMapInterface.v | 4 ++-- theories/FSets/FMapList.v | 4 ++-- theories/FSets/FMapPositive.v | 4 ++-- theories/FSets/FMapWeakList.v | 4 ++-- theories/FSets/FMaps.v | 4 ++-- theories/FSets/FSetAVL.v | 4 ++-- theories/FSets/FSetBridge.v | 4 ++-- theories/FSets/FSetCompat.v | 4 ++-- theories/FSets/FSetDecide.v | 4 ++-- theories/FSets/FSetEqProperties.v | 4 ++-- theories/FSets/FSetFacts.v | 4 ++-- theories/FSets/FSetInterface.v | 4 ++-- theories/FSets/FSetList.v | 4 ++-- theories/FSets/FSetPositive.v | 4 ++-- theories/FSets/FSetProperties.v | 4 ++-- theories/FSets/FSetToFiniteSet.v | 4 ++-- theories/FSets/FSetWeakList.v | 4 ++-- theories/FSets/FSets.v | 4 ++-- theories/Floats/FloatAxioms.v | 10 ++++++++++ theories/Floats/FloatClass.v | 10 ++++++++++ theories/Floats/FloatLemmas.v | 10 ++++++++++ theories/Floats/FloatOps.v | 10 ++++++++++ theories/Floats/Floats.v | 10 ++++++++++ theories/Floats/PrimFloat.v | 10 ++++++++++ theories/Floats/SpecFloat.v | 10 ++++++++++ theories/Init/Byte.v | 4 ++-- theories/Init/Datatypes.v | 4 ++-- theories/Init/Decimal.v | 4 ++-- theories/Init/Logic.v | 4 ++-- theories/Init/Logic_Type.v | 4 ++-- theories/Init/Nat.v | 4 ++-- theories/Init/Notations.v | 4 ++-- theories/Init/Peano.v | 4 ++-- theories/Init/Prelude.v | 4 ++-- theories/Init/Specif.v | 4 ++-- theories/Init/Tactics.v | 4 ++-- theories/Init/Wf.v | 4 ++-- theories/Lists/List.v | 4 ++-- theories/Lists/ListDec.v | 4 ++-- theories/Lists/ListSet.v | 4 ++-- theories/Lists/ListTactics.v | 4 ++-- theories/Lists/SetoidList.v | 4 ++-- theories/Lists/SetoidPermutation.v | 4 ++-- theories/Lists/StreamMemo.v | 4 ++-- theories/Lists/Streams.v | 4 ++-- theories/Logic/Berardi.v | 4 ++-- theories/Logic/ChoiceFacts.v | 4 ++-- theories/Logic/Classical.v | 4 ++-- theories/Logic/ClassicalChoice.v | 4 ++-- theories/Logic/ClassicalDescription.v | 4 ++-- theories/Logic/ClassicalEpsilon.v | 4 ++-- theories/Logic/ClassicalFacts.v | 4 ++-- theories/Logic/ClassicalUniqueChoice.v | 4 ++-- theories/Logic/Classical_Pred_Type.v | 4 ++-- theories/Logic/Classical_Prop.v | 4 ++-- theories/Logic/ConstructiveEpsilon.v | 4 ++-- theories/Logic/Decidable.v | 4 ++-- theories/Logic/Description.v | 4 ++-- theories/Logic/Diaconescu.v | 4 ++-- theories/Logic/Epsilon.v | 4 ++-- theories/Logic/Eqdep.v | 4 ++-- theories/Logic/EqdepFacts.v | 4 ++-- theories/Logic/Eqdep_dec.v | 4 ++-- theories/Logic/ExtensionalFunctionRepresentative.v | 4 ++-- theories/Logic/ExtensionalityFacts.v | 4 ++-- theories/Logic/FinFun.v | 4 ++-- theories/Logic/FunctionalExtensionality.v | 4 ++-- theories/Logic/HLevels.v | 4 ++-- theories/Logic/Hurkens.v | 4 ++-- theories/Logic/IndefiniteDescription.v | 4 ++-- theories/Logic/JMeq.v | 4 ++-- theories/Logic/ProofIrrelevance.v | 4 ++-- theories/Logic/ProofIrrelevanceFacts.v | 4 ++-- theories/Logic/PropExtensionality.v | 4 ++-- theories/Logic/PropExtensionalityFacts.v | 4 ++-- theories/Logic/PropFacts.v | 4 ++-- theories/Logic/RelationalChoice.v | 4 ++-- theories/Logic/SetIsType.v | 4 ++-- theories/Logic/SetoidChoice.v | 4 ++-- theories/Logic/StrictProp.v | 4 ++-- theories/Logic/WKL.v | 4 ++-- theories/Logic/WeakFan.v | 4 ++-- theories/MSets/MSetAVL.v | 4 ++-- theories/MSets/MSetDecide.v | 4 ++-- theories/MSets/MSetEqProperties.v | 4 ++-- theories/MSets/MSetFacts.v | 4 ++-- theories/MSets/MSetGenTree.v | 4 ++-- theories/MSets/MSetInterface.v | 4 ++-- theories/MSets/MSetList.v | 4 ++-- theories/MSets/MSetPositive.v | 4 ++-- theories/MSets/MSetProperties.v | 4 ++-- theories/MSets/MSetRBT.v | 4 ++-- theories/MSets/MSetToFiniteSet.v | 4 ++-- theories/MSets/MSetWeakList.v | 4 ++-- theories/MSets/MSets.v | 4 ++-- theories/NArith/BinNat.v | 4 ++-- theories/NArith/BinNatDef.v | 4 ++-- theories/NArith/NArith.v | 4 ++-- theories/NArith/Ndec.v | 4 ++-- theories/NArith/Ndigits.v | 4 ++-- theories/NArith/Ndist.v | 4 ++-- theories/NArith/Ndiv_def.v | 4 ++-- theories/NArith/Ngcd_def.v | 4 ++-- theories/NArith/Nnat.v | 4 ++-- theories/NArith/Nsqrt_def.v | 4 ++-- theories/Numbers/AltBinNotations.v | 4 ++-- theories/Numbers/BinNums.v | 4 ++-- theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 4 ++-- theories/Numbers/Cyclic/Abstract/DoubleType.v | 4 ++-- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 4 ++-- theories/Numbers/Cyclic/Int31/Cyclic31.v | 4 ++-- theories/Numbers/Cyclic/Int31/Int31.v | 4 ++-- theories/Numbers/Cyclic/Int31/Ring31.v | 4 ++-- theories/Numbers/Cyclic/Int63/Cyclic63.v | 4 ++-- theories/Numbers/Cyclic/Int63/Int63.v | 4 ++-- theories/Numbers/Cyclic/Int63/Ring63.v | 4 ++-- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 4 ++-- theories/Numbers/DecimalFacts.v | 4 ++-- theories/Numbers/DecimalN.v | 4 ++-- theories/Numbers/DecimalNat.v | 4 ++-- theories/Numbers/DecimalPos.v | 4 ++-- theories/Numbers/DecimalString.v | 4 ++-- theories/Numbers/DecimalZ.v | 4 ++-- theories/Numbers/Integer/Abstract/ZAdd.v | 4 ++-- theories/Numbers/Integer/Abstract/ZAddOrder.v | 4 ++-- theories/Numbers/Integer/Abstract/ZAxioms.v | 4 ++-- theories/Numbers/Integer/Abstract/ZBase.v | 4 ++-- theories/Numbers/Integer/Abstract/ZBits.v | 4 ++-- theories/Numbers/Integer/Abstract/ZDivEucl.v | 4 ++-- theories/Numbers/Integer/Abstract/ZDivFloor.v | 4 ++-- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 4 ++-- theories/Numbers/Integer/Abstract/ZGcd.v | 4 ++-- theories/Numbers/Integer/Abstract/ZLcm.v | 4 ++-- theories/Numbers/Integer/Abstract/ZLt.v | 4 ++-- theories/Numbers/Integer/Abstract/ZMaxMin.v | 4 ++-- theories/Numbers/Integer/Abstract/ZMul.v | 4 ++-- theories/Numbers/Integer/Abstract/ZMulOrder.v | 4 ++-- theories/Numbers/Integer/Abstract/ZParity.v | 4 ++-- theories/Numbers/Integer/Abstract/ZPow.v | 4 ++-- theories/Numbers/Integer/Abstract/ZProperties.v | 4 ++-- theories/Numbers/Integer/Abstract/ZSgnAbs.v | 4 ++-- theories/Numbers/Integer/Binary/ZBinary.v | 4 ++-- theories/Numbers/Integer/NatPairs/ZNatPairs.v | 4 ++-- theories/Numbers/NaryFunctions.v | 4 ++-- theories/Numbers/NatInt/NZAdd.v | 4 ++-- theories/Numbers/NatInt/NZAddOrder.v | 4 ++-- theories/Numbers/NatInt/NZAxioms.v | 4 ++-- theories/Numbers/NatInt/NZBase.v | 4 ++-- theories/Numbers/NatInt/NZBits.v | 4 ++-- theories/Numbers/NatInt/NZDiv.v | 4 ++-- theories/Numbers/NatInt/NZDomain.v | 4 ++-- theories/Numbers/NatInt/NZGcd.v | 4 ++-- theories/Numbers/NatInt/NZLog.v | 4 ++-- theories/Numbers/NatInt/NZMul.v | 4 ++-- theories/Numbers/NatInt/NZMulOrder.v | 4 ++-- theories/Numbers/NatInt/NZOrder.v | 4 ++-- theories/Numbers/NatInt/NZParity.v | 4 ++-- theories/Numbers/NatInt/NZPow.v | 4 ++-- theories/Numbers/NatInt/NZProperties.v | 4 ++-- theories/Numbers/NatInt/NZSqrt.v | 4 ++-- theories/Numbers/Natural/Abstract/NAdd.v | 4 ++-- theories/Numbers/Natural/Abstract/NAddOrder.v | 4 ++-- theories/Numbers/Natural/Abstract/NAxioms.v | 4 ++-- theories/Numbers/Natural/Abstract/NBase.v | 4 ++-- theories/Numbers/Natural/Abstract/NBits.v | 4 ++-- theories/Numbers/Natural/Abstract/NDefOps.v | 4 ++-- theories/Numbers/Natural/Abstract/NDiv.v | 4 ++-- theories/Numbers/Natural/Abstract/NGcd.v | 4 ++-- theories/Numbers/Natural/Abstract/NIso.v | 4 ++-- theories/Numbers/Natural/Abstract/NLcm.v | 4 ++-- theories/Numbers/Natural/Abstract/NLog.v | 4 ++-- theories/Numbers/Natural/Abstract/NMaxMin.v | 4 ++-- theories/Numbers/Natural/Abstract/NMulOrder.v | 4 ++-- theories/Numbers/Natural/Abstract/NOrder.v | 4 ++-- theories/Numbers/Natural/Abstract/NParity.v | 4 ++-- theories/Numbers/Natural/Abstract/NPow.v | 4 ++-- theories/Numbers/Natural/Abstract/NProperties.v | 4 ++-- theories/Numbers/Natural/Abstract/NSqrt.v | 4 ++-- theories/Numbers/Natural/Abstract/NStrongRec.v | 4 ++-- theories/Numbers/Natural/Abstract/NSub.v | 4 ++-- theories/Numbers/Natural/Binary/NBinary.v | 4 ++-- theories/Numbers/Natural/Peano/NPeano.v | 4 ++-- theories/Numbers/NumPrelude.v | 4 ++-- theories/PArith/BinPos.v | 4 ++-- theories/PArith/BinPosDef.v | 4 ++-- theories/PArith/PArith.v | 4 ++-- theories/PArith/POrderedType.v | 4 ++-- theories/PArith/Pnat.v | 4 ++-- theories/Program/Basics.v | 4 ++-- theories/Program/Combinators.v | 4 ++-- theories/Program/Equality.v | 4 ++-- theories/Program/Program.v | 4 ++-- theories/Program/Subset.v | 4 ++-- theories/Program/Syntax.v | 4 ++-- theories/Program/Tactics.v | 4 ++-- theories/Program/Utils.v | 4 ++-- theories/Program/Wf.v | 4 ++-- theories/QArith/QArith.v | 4 ++-- theories/QArith/QArith_base.v | 4 ++-- theories/QArith/QOrderedType.v | 4 ++-- theories/QArith/Qabs.v | 4 ++-- theories/QArith/Qcabs.v | 4 ++-- theories/QArith/Qcanon.v | 4 ++-- theories/QArith/Qfield.v | 4 ++-- theories/QArith/Qminmax.v | 4 ++-- theories/QArith/Qpower.v | 4 ++-- theories/QArith/Qreals.v | 4 ++-- theories/QArith/Qreduction.v | 4 ++-- theories/QArith/Qring.v | 4 ++-- theories/QArith/Qround.v | 4 ++-- theories/Reals/Alembert.v | 4 ++-- theories/Reals/AltSeries.v | 4 ++-- theories/Reals/ArithProp.v | 4 ++-- theories/Reals/Binomial.v | 4 ++-- theories/Reals/Cauchy_prod.v | 4 ++-- theories/Reals/ClassicalDedekindReals.v | 4 ++-- theories/Reals/ConstructiveCauchyReals.v | 4 ++-- theories/Reals/ConstructiveCauchyRealsMult.v | 4 ++-- theories/Reals/ConstructiveRcomplete.v | 4 ++-- theories/Reals/ConstructiveReals.v | 4 ++-- theories/Reals/ConstructiveRealsLUB.v | 4 ++-- theories/Reals/ConstructiveRealsMorphisms.v | 4 ++-- theories/Reals/Cos_plus.v | 4 ++-- theories/Reals/Cos_rel.v | 4 ++-- theories/Reals/DiscrR.v | 4 ++-- theories/Reals/Exp_prop.v | 4 ++-- theories/Reals/Integration.v | 4 ++-- theories/Reals/MVT.v | 4 ++-- theories/Reals/Machin.v | 4 ++-- theories/Reals/NewtonInt.v | 4 ++-- theories/Reals/PSeries_reg.v | 4 ++-- theories/Reals/PartSum.v | 4 ++-- theories/Reals/RIneq.v | 4 ++-- theories/Reals/RList.v | 4 ++-- theories/Reals/ROrderedType.v | 4 ++-- theories/Reals/R_Ifp.v | 4 ++-- theories/Reals/R_sqr.v | 4 ++-- theories/Reals/R_sqrt.v | 4 ++-- theories/Reals/Ranalysis.v | 4 ++-- theories/Reals/Ranalysis1.v | 4 ++-- theories/Reals/Ranalysis2.v | 4 ++-- theories/Reals/Ranalysis3.v | 4 ++-- theories/Reals/Ranalysis4.v | 4 ++-- theories/Reals/Ranalysis5.v | 4 ++-- theories/Reals/Ranalysis_reg.v | 4 ++-- theories/Reals/Ratan.v | 4 ++-- theories/Reals/Raxioms.v | 4 ++-- theories/Reals/Rbase.v | 4 ++-- theories/Reals/Rbasic_fun.v | 4 ++-- theories/Reals/Rcomplete.v | 4 ++-- theories/Reals/Rdefinitions.v | 4 ++-- theories/Reals/Rderiv.v | 4 ++-- theories/Reals/Reals.v | 4 ++-- theories/Reals/Rfunctions.v | 4 ++-- theories/Reals/Rgeom.v | 4 ++-- theories/Reals/RiemannInt.v | 4 ++-- theories/Reals/RiemannInt_SF.v | 4 ++-- theories/Reals/Rlimit.v | 4 ++-- theories/Reals/Rlogic.v | 4 ++-- theories/Reals/Rminmax.v | 4 ++-- theories/Reals/Rpow_def.v | 4 ++-- theories/Reals/Rpower.v | 4 ++-- theories/Reals/Rprod.v | 4 ++-- theories/Reals/Rregisternames.v | 4 ++-- theories/Reals/Rseries.v | 4 ++-- theories/Reals/Rsigma.v | 4 ++-- theories/Reals/Rsqrt_def.v | 4 ++-- theories/Reals/Rtopology.v | 4 ++-- theories/Reals/Rtrigo.v | 4 ++-- theories/Reals/Rtrigo1.v | 4 ++-- theories/Reals/Rtrigo_alt.v | 4 ++-- theories/Reals/Rtrigo_calc.v | 4 ++-- theories/Reals/Rtrigo_def.v | 4 ++-- theories/Reals/Rtrigo_fun.v | 4 ++-- theories/Reals/Rtrigo_reg.v | 4 ++-- theories/Reals/Runcountable.v | 4 ++-- theories/Reals/SeqProp.v | 4 ++-- theories/Reals/SeqSeries.v | 4 ++-- theories/Reals/SplitAbsolu.v | 4 ++-- theories/Reals/SplitRmult.v | 4 ++-- theories/Reals/Sqrt_reg.v | 4 ++-- theories/Relations/Operators_Properties.v | 4 ++-- theories/Relations/Relation_Definitions.v | 4 ++-- theories/Relations/Relation_Operators.v | 4 ++-- theories/Relations/Relations.v | 4 ++-- theories/Setoids/Setoid.v | 4 ++-- theories/Sets/Classical_sets.v | 4 ++-- theories/Sets/Constructive_sets.v | 4 ++-- theories/Sets/Cpo.v | 4 ++-- theories/Sets/Ensembles.v | 4 ++-- theories/Sets/Finite_sets.v | 4 ++-- theories/Sets/Finite_sets_facts.v | 4 ++-- theories/Sets/Image.v | 4 ++-- theories/Sets/Infinite_sets.v | 4 ++-- theories/Sets/Integers.v | 4 ++-- theories/Sets/Multiset.v | 4 ++-- theories/Sets/Partial_Order.v | 4 ++-- theories/Sets/Permut.v | 4 ++-- theories/Sets/Powerset.v | 4 ++-- theories/Sets/Powerset_Classical_facts.v | 4 ++-- theories/Sets/Powerset_facts.v | 4 ++-- theories/Sets/Relations_1.v | 4 ++-- theories/Sets/Relations_1_facts.v | 4 ++-- theories/Sets/Relations_2.v | 4 ++-- theories/Sets/Relations_2_facts.v | 4 ++-- theories/Sets/Relations_3.v | 4 ++-- theories/Sets/Relations_3_facts.v | 4 ++-- theories/Sets/Uniset.v | 4 ++-- theories/Sorting/Heap.v | 4 ++-- theories/Sorting/Mergesort.v | 4 ++-- theories/Sorting/PermutEq.v | 4 ++-- theories/Sorting/PermutSetoid.v | 4 ++-- theories/Sorting/Permutation.v | 4 ++-- theories/Sorting/Sorted.v | 4 ++-- theories/Sorting/Sorting.v | 4 ++-- theories/Strings/Ascii.v | 4 ++-- theories/Strings/BinaryString.v | 4 ++-- theories/Strings/Byte.v | 4 ++-- theories/Strings/ByteVector.v | 4 ++-- theories/Strings/HexString.v | 4 ++-- theories/Strings/OctalString.v | 4 ++-- theories/Strings/String.v | 4 ++-- theories/Structures/DecidableType.v | 4 ++-- theories/Structures/DecidableTypeEx.v | 4 ++-- theories/Structures/Equalities.v | 4 ++-- theories/Structures/EqualitiesFacts.v | 4 ++-- theories/Structures/GenericMinMax.v | 4 ++-- theories/Structures/OrderedType.v | 4 ++-- theories/Structures/OrderedTypeAlt.v | 4 ++-- theories/Structures/OrderedTypeEx.v | 4 ++-- theories/Structures/Orders.v | 4 ++-- theories/Structures/OrdersAlt.v | 4 ++-- theories/Structures/OrdersEx.v | 4 ++-- theories/Structures/OrdersFacts.v | 4 ++-- theories/Structures/OrdersLists.v | 4 ++-- theories/Structures/OrdersTac.v | 4 ++-- theories/Unicode/Utf8.v | 4 ++-- theories/Unicode/Utf8_core.v | 4 ++-- theories/Vectors/Fin.v | 4 ++-- theories/Vectors/Vector.v | 4 ++-- theories/Vectors/VectorDef.v | 4 ++-- theories/Vectors/VectorEq.v | 4 ++-- theories/Vectors/VectorSpec.v | 4 ++-- theories/Wellfounded/Disjoint_Union.v | 4 ++-- theories/Wellfounded/Inclusion.v | 4 ++-- theories/Wellfounded/Inverse_Image.v | 4 ++-- theories/Wellfounded/Lexicographic_Exponentiation.v | 4 ++-- theories/Wellfounded/Lexicographic_Product.v | 4 ++-- theories/Wellfounded/Transitive_Closure.v | 4 ++-- theories/Wellfounded/Union.v | 4 ++-- theories/Wellfounded/Well_Ordering.v | 4 ++-- theories/Wellfounded/Wellfounded.v | 4 ++-- theories/ZArith/BinInt.v | 4 ++-- theories/ZArith/BinIntDef.v | 4 ++-- theories/ZArith/Int.v | 4 ++-- theories/ZArith/Wf_Z.v | 4 ++-- theories/ZArith/ZArith.v | 4 ++-- theories/ZArith/ZArith_base.v | 4 ++-- theories/ZArith/ZArith_dec.v | 4 ++-- theories/ZArith/Zabs.v | 4 ++-- theories/ZArith/Zbool.v | 4 ++-- theories/ZArith/Zcompare.v | 4 ++-- theories/ZArith/Zcomplements.v | 4 ++-- theories/ZArith/Zdigits.v | 4 ++-- theories/ZArith/Zdiv.v | 4 ++-- theories/ZArith/Zeuclid.v | 4 ++-- theories/ZArith/Zeven.v | 4 ++-- theories/ZArith/Zgcd_alt.v | 4 ++-- theories/ZArith/Zhints.v | 4 ++-- theories/ZArith/Zmax.v | 4 ++-- theories/ZArith/Zmin.v | 4 ++-- theories/ZArith/Zminmax.v | 4 ++-- theories/ZArith/Zmisc.v | 4 ++-- theories/ZArith/Znat.v | 4 ++-- theories/ZArith/Znumtheory.v | 4 ++-- theories/ZArith/Zorder.v | 4 ++-- theories/ZArith/Zpow_alt.v | 4 ++-- theories/ZArith/Zpow_def.v | 4 ++-- theories/ZArith/Zpow_facts.v | 4 ++-- theories/ZArith/Zpower.v | 4 ++-- theories/ZArith/Zquot.v | 4 ++-- theories/ZArith/Zwf.v | 4 ++-- theories/ZArith/auxiliary.v | 4 ++-- theories/extraction/ExtrOCamlFloats.v | 4 ++-- theories/extraction/ExtrOCamlInt63.v | 4 ++-- theories/extraction/ExtrOcamlBasic.v | 4 ++-- theories/extraction/ExtrOcamlBigIntConv.v | 4 ++-- theories/extraction/ExtrOcamlChar.v | 4 ++-- theories/extraction/ExtrOcamlIntConv.v | 4 ++-- theories/extraction/ExtrOcamlNatBigInt.v | 4 ++-- theories/extraction/ExtrOcamlNatInt.v | 4 ++-- theories/extraction/ExtrOcamlNativeString.v | 4 ++-- theories/extraction/ExtrOcamlString.v | 4 ++-- theories/extraction/ExtrOcamlZBigInt.v | 4 ++-- theories/extraction/ExtrOcamlZInt.v | 4 ++-- theories/extraction/Extraction.v | 4 ++-- theories/funind/FunInd.v | 4 ++-- theories/funind/Recdef.v | 4 ++-- theories/micromega/DeclConstant.v | 4 ++-- theories/micromega/Env.v | 4 ++-- theories/micromega/EnvRing.v | 4 ++-- theories/micromega/Lia.v | 4 ++-- theories/micromega/Lqa.v | 4 ++-- theories/micromega/Lra.v | 4 ++-- theories/micromega/MExtraction.v | 4 ++-- theories/micromega/OrderedRing.v | 4 ++-- theories/micromega/Psatz.v | 4 ++-- theories/micromega/QMicromega.v | 4 ++-- theories/micromega/RMicromega.v | 4 ++-- theories/micromega/Refl.v | 4 ++-- theories/micromega/RingMicromega.v | 4 ++-- theories/micromega/Tauto.v | 4 ++-- theories/micromega/VarMap.v | 4 ++-- theories/micromega/ZCoeff.v | 4 ++-- theories/micromega/ZMicromega.v | 4 ++-- theories/micromega/Zify.v | 4 ++-- theories/micromega/ZifyBool.v | 4 ++-- theories/micromega/ZifyClasses.v | 4 ++-- theories/micromega/ZifyComparison.v | 4 ++-- theories/micromega/ZifyInst.v | 4 ++-- theories/micromega/Ztac.v | 4 ++-- theories/nsatz/Nsatz.v | 4 ++-- theories/omega/Omega.v | 4 ++-- theories/omega/OmegaLemmas.v | 4 ++-- theories/omega/OmegaPlugin.v | 4 ++-- theories/omega/OmegaTactic.v | 4 ++-- theories/omega/PreOmega.v | 4 ++-- theories/rtauto/Bintree.v | 4 ++-- theories/rtauto/Rtauto.v | 4 ++-- theories/setoid_ring/Algebra_syntax.v | 4 ++-- theories/setoid_ring/ArithRing.v | 4 ++-- theories/setoid_ring/BinList.v | 4 ++-- theories/setoid_ring/Cring.v | 4 ++-- theories/setoid_ring/Field.v | 4 ++-- theories/setoid_ring/Field_tac.v | 4 ++-- theories/setoid_ring/Field_theory.v | 4 ++-- theories/setoid_ring/InitialRing.v | 4 ++-- theories/setoid_ring/Integral_domain.v | 4 ++-- theories/setoid_ring/NArithRing.v | 4 ++-- theories/setoid_ring/Ncring.v | 4 ++-- theories/setoid_ring/Ncring_initial.v | 4 ++-- theories/setoid_ring/Ncring_polynom.v | 4 ++-- theories/setoid_ring/Ncring_tac.v | 4 ++-- theories/setoid_ring/RealField.v | 4 ++-- theories/setoid_ring/Ring.v | 4 ++-- theories/setoid_ring/Ring_base.v | 4 ++-- theories/setoid_ring/Ring_polynom.v | 4 ++-- theories/setoid_ring/Ring_tac.v | 4 ++-- theories/setoid_ring/Ring_theory.v | 4 ++-- theories/setoid_ring/Rings_Q.v | 4 ++-- theories/setoid_ring/Rings_R.v | 4 ++-- theories/setoid_ring/Rings_Z.v | 4 ++-- theories/setoid_ring/ZArithRing.v | 4 ++-- theories/ssr/ssrbool.v | 4 ++-- theories/ssr/ssrclasses.v | 4 ++-- theories/ssr/ssreflect.v | 4 ++-- theories/ssr/ssrfun.v | 4 ++-- theories/ssr/ssrsetoid.v | 4 ++-- theories/ssr/ssrunder.v | 4 ++-- theories/ssrmatching/ssrmatching.v | 4 ++-- tools/CoqMakefile.in | 15 +++++++++------ tools/coq_dune.ml | 4 ++-- tools/coq_makefile.ml | 4 ++-- tools/coq_tex.ml | 4 ++-- tools/coqdep.ml | 4 ++-- tools/coqdep_boot.ml | 4 ++-- tools/coqdep_common.ml | 4 ++-- tools/coqdep_common.mli | 4 ++-- tools/coqdep_lexer.mli | 4 ++-- tools/coqdep_lexer.mll | 4 ++-- tools/coqdoc/alpha.ml | 4 ++-- tools/coqdoc/alpha.mli | 4 ++-- tools/coqdoc/cdglobals.ml | 4 ++-- tools/coqdoc/cpretty.mli | 4 ++-- tools/coqdoc/cpretty.mll | 4 ++-- tools/coqdoc/index.ml | 4 ++-- tools/coqdoc/index.mli | 4 ++-- tools/coqdoc/main.ml | 4 ++-- tools/coqdoc/output.ml | 4 ++-- tools/coqdoc/output.mli | 4 ++-- tools/coqdoc/tokens.ml | 4 ++-- tools/coqdoc/tokens.mli | 4 ++-- tools/coqwc.mll | 4 ++-- tools/coqworkmgr.ml | 4 ++-- tools/ocamllibdep.mll | 4 ++-- topbin/coqc_bin.ml | 4 ++-- topbin/coqproofworker_bin.ml | 4 ++-- topbin/coqqueryworker_bin.ml | 4 ++-- topbin/coqtacticworker_bin.ml | 4 ++-- topbin/coqtop_bin.ml | 4 ++-- topbin/coqtop_byte_bin.ml | 4 ++-- toplevel/ccompile.ml | 4 ++-- toplevel/ccompile.mli | 4 ++-- toplevel/coqargs.ml | 4 ++-- toplevel/coqargs.mli | 4 ++-- toplevel/coqc.ml | 4 ++-- toplevel/coqc.mli | 4 ++-- toplevel/coqcargs.ml | 4 ++-- toplevel/coqcargs.mli | 4 ++-- toplevel/coqinit.ml | 4 ++-- toplevel/coqinit.mli | 4 ++-- toplevel/coqloop.ml | 4 ++-- toplevel/coqloop.mli | 4 ++-- toplevel/coqtop.ml | 4 ++-- toplevel/coqtop.mli | 4 ++-- toplevel/g_toplevel.mlg | 4 ++-- toplevel/usage.ml | 4 ++-- toplevel/usage.mli | 4 ++-- toplevel/vernac.ml | 4 ++-- toplevel/vernac.mli | 4 ++-- toplevel/workerLoop.ml | 4 ++-- toplevel/workerLoop.mli | 4 ++-- user-contrib/Ltac2/Array.v | 4 ++-- user-contrib/Ltac2/Bool.v | 4 ++-- user-contrib/Ltac2/Char.v | 4 ++-- user-contrib/Ltac2/Constr.v | 4 ++-- user-contrib/Ltac2/Control.v | 4 ++-- user-contrib/Ltac2/Env.v | 4 ++-- user-contrib/Ltac2/Fresh.v | 4 ++-- user-contrib/Ltac2/Ident.v | 4 ++-- user-contrib/Ltac2/Init.v | 4 ++-- user-contrib/Ltac2/Int.v | 4 ++-- user-contrib/Ltac2/List.v | 4 ++-- user-contrib/Ltac2/Ltac1.v | 4 ++-- user-contrib/Ltac2/Ltac2.v | 4 ++-- user-contrib/Ltac2/Message.v | 4 ++-- user-contrib/Ltac2/Notations.v | 4 ++-- user-contrib/Ltac2/Option.v | 4 ++-- user-contrib/Ltac2/Pattern.v | 4 ++-- user-contrib/Ltac2/Std.v | 4 ++-- user-contrib/Ltac2/String.v | 4 ++-- user-contrib/Ltac2/g_ltac2.mlg | 4 ++-- user-contrib/Ltac2/tac2core.ml | 4 ++-- user-contrib/Ltac2/tac2core.mli | 4 ++-- user-contrib/Ltac2/tac2dyn.ml | 4 ++-- user-contrib/Ltac2/tac2dyn.mli | 4 ++-- user-contrib/Ltac2/tac2entries.ml | 4 ++-- user-contrib/Ltac2/tac2entries.mli | 4 ++-- user-contrib/Ltac2/tac2env.ml | 4 ++-- user-contrib/Ltac2/tac2env.mli | 4 ++-- user-contrib/Ltac2/tac2expr.mli | 4 ++-- user-contrib/Ltac2/tac2extffi.ml | 4 ++-- user-contrib/Ltac2/tac2extffi.mli | 4 ++-- user-contrib/Ltac2/tac2ffi.ml | 4 ++-- user-contrib/Ltac2/tac2ffi.mli | 4 ++-- user-contrib/Ltac2/tac2intern.ml | 4 ++-- user-contrib/Ltac2/tac2intern.mli | 4 ++-- user-contrib/Ltac2/tac2interp.ml | 4 ++-- user-contrib/Ltac2/tac2interp.mli | 4 ++-- user-contrib/Ltac2/tac2match.ml | 4 ++-- user-contrib/Ltac2/tac2match.mli | 4 ++-- user-contrib/Ltac2/tac2print.ml | 4 ++-- user-contrib/Ltac2/tac2print.mli | 4 ++-- user-contrib/Ltac2/tac2qexpr.mli | 4 ++-- user-contrib/Ltac2/tac2quote.ml | 4 ++-- user-contrib/Ltac2/tac2quote.mli | 4 ++-- user-contrib/Ltac2/tac2stdlib.ml | 4 ++-- user-contrib/Ltac2/tac2stdlib.mli | 4 ++-- user-contrib/Ltac2/tac2tactics.ml | 4 ++-- user-contrib/Ltac2/tac2tactics.mli | 4 ++-- user-contrib/Ltac2/tac2types.mli | 4 ++-- vernac/assumptions.ml | 4 ++-- vernac/assumptions.mli | 4 ++-- vernac/attributes.ml | 4 ++-- vernac/attributes.mli | 4 ++-- vernac/auto_ind_decl.ml | 4 ++-- vernac/auto_ind_decl.mli | 4 ++-- vernac/canonical.ml | 4 ++-- vernac/canonical.mli | 4 ++-- vernac/classes.ml | 4 ++-- vernac/classes.mli | 4 ++-- vernac/comArguments.ml | 4 ++-- vernac/comArguments.mli | 4 ++-- vernac/comAssumption.ml | 4 ++-- vernac/comAssumption.mli | 4 ++-- vernac/comCoercion.ml | 4 ++-- vernac/comCoercion.mli | 4 ++-- vernac/comDefinition.ml | 4 ++-- vernac/comDefinition.mli | 4 ++-- vernac/comFixpoint.ml | 4 ++-- vernac/comFixpoint.mli | 4 ++-- vernac/comInductive.ml | 4 ++-- vernac/comInductive.mli | 4 ++-- vernac/comPrimitive.ml | 4 ++-- vernac/comPrimitive.mli | 4 ++-- vernac/comProgramFixpoint.ml | 4 ++-- vernac/comProgramFixpoint.mli | 4 ++-- vernac/declareDef.ml | 4 ++-- vernac/declareDef.mli | 4 ++-- vernac/declareInd.ml | 4 ++-- vernac/declareInd.mli | 4 ++-- vernac/declareObl.ml | 4 ++-- vernac/declareObl.mli | 4 ++-- vernac/declareUniv.ml | 4 ++-- vernac/declareUniv.mli | 4 ++-- vernac/declaremods.ml | 4 ++-- vernac/declaremods.mli | 4 ++-- vernac/egramcoq.ml | 4 ++-- vernac/egramcoq.mli | 4 ++-- vernac/egramml.ml | 4 ++-- vernac/egramml.mli | 4 ++-- vernac/g_proofs.mlg | 4 ++-- vernac/g_vernac.mlg | 4 ++-- vernac/himsg.ml | 4 ++-- vernac/himsg.mli | 4 ++-- vernac/indschemes.ml | 4 ++-- vernac/indschemes.mli | 4 ++-- vernac/lemmas.ml | 4 ++-- vernac/lemmas.mli | 4 ++-- vernac/library.ml | 4 ++-- vernac/library.mli | 4 ++-- vernac/loadpath.ml | 4 ++-- vernac/loadpath.mli | 4 ++-- vernac/locality.ml | 4 ++-- vernac/locality.mli | 4 ++-- vernac/metasyntax.ml | 4 ++-- vernac/metasyntax.mli | 4 ++-- vernac/mltop.ml | 4 ++-- vernac/mltop.mli | 4 ++-- vernac/obligations.ml | 4 ++-- vernac/obligations.mli | 4 ++-- vernac/ppvernac.ml | 4 ++-- vernac/ppvernac.mli | 4 ++-- vernac/prettyp.ml | 4 ++-- vernac/prettyp.mli | 4 ++-- vernac/proof_using.ml | 4 ++-- vernac/proof_using.mli | 4 ++-- vernac/pvernac.ml | 4 ++-- vernac/pvernac.mli | 4 ++-- vernac/recLemmas.ml | 4 ++-- vernac/recLemmas.mli | 4 ++-- vernac/record.ml | 4 ++-- vernac/record.mli | 4 ++-- vernac/search.ml | 4 ++-- vernac/search.mli | 4 ++-- vernac/topfmt.ml | 4 ++-- vernac/topfmt.mli | 4 ++-- vernac/vernacentries.ml | 4 ++-- vernac/vernacentries.mli | 4 ++-- vernac/vernacexpr.ml | 4 ++-- vernac/vernacextend.ml | 4 ++-- vernac/vernacextend.mli | 4 ++-- vernac/vernacinterp.ml | 4 ++-- vernac/vernacinterp.mli | 4 ++-- vernac/vernacprop.ml | 4 ++-- vernac/vernacprop.mli | 4 ++-- vernac/vernacstate.ml | 4 ++-- vernac/vernacstate.mli | 4 ++-- 1609 files changed, 3340 insertions(+), 3196 deletions(-) diff --git a/Makefile b/Makefile index c416172dbf..d83ffeac3e 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 5be7587091..27696e8856 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -1,3 +1,13 @@ +/************************************************************************/ +/* * The Coq Proof Assistant / The Coq Development Team */ +/* v * Copyright INRIA, CNRS and contributors */ +/* > 1) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index af08ea18c1..1316dfe069 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(*