From 629fbc743f8b5e7623a6834f19885b2e379cb782 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 27 Feb 2018 17:02:31 +0100 Subject: Update headers following #6543. --- Makefile | 16 +++++++++------- Makefile.build | 16 +++++++++------- Makefile.checker | 16 +++++++++------- Makefile.ci | 10 ++++++++++ Makefile.common | 16 +++++++++------- Makefile.dev | 16 +++++++++------- Makefile.doc | 16 +++++++++------- Makefile.ide | 16 +++++++++------- Makefile.install | 16 +++++++++------- checker/check.ml | 10 ++++++---- checker/check.mli | 10 ++++++---- checker/check_stat.ml | 10 ++++++---- checker/check_stat.mli | 10 ++++++---- checker/checker.ml | 10 ++++++---- checker/checker.mli | 10 ++++++---- checker/cic.mli | 10 ++++++---- checker/closure.ml | 10 ++++++---- checker/closure.mli | 10 ++++++---- checker/indtypes.ml | 10 ++++++---- checker/indtypes.mli | 10 ++++++---- checker/inductive.ml | 10 ++++++---- checker/inductive.mli | 10 ++++++---- checker/main.mli | 10 ++++++---- checker/mod_checking.mli | 10 ++++++---- checker/modops.ml | 10 ++++++---- checker/modops.mli | 10 ++++++---- checker/print.ml | 10 ++++++---- checker/print.mli | 10 ++++++---- checker/reduction.ml | 10 ++++++---- checker/reduction.mli | 10 ++++++---- checker/safe_typing.ml | 10 ++++++---- checker/safe_typing.mli | 10 ++++++---- checker/subtyping.ml | 10 ++++++---- checker/subtyping.mli | 10 ++++++---- checker/term.ml | 10 ++++++---- checker/type_errors.ml | 10 ++++++---- checker/type_errors.mli | 10 ++++++---- checker/typeops.ml | 10 ++++++---- checker/typeops.mli | 10 ++++++---- checker/univ.ml | 10 ++++++---- checker/univ.mli | 10 ++++++---- checker/validate.ml | 10 ++++++---- checker/validate.mli | 10 ++++++---- checker/values.ml | 12 +++++++----- checker/values.mli | 10 ++++++---- checker/votour.ml | 10 ++++++---- checker/votour.mli | 10 ++++++---- clib/backtrace.ml | 16 +++++++++------- clib/backtrace.mli | 16 +++++++++------- clib/bigint.ml | 10 ++++++---- clib/bigint.mli | 10 ++++++---- clib/cArray.ml | 16 +++++++++------- clib/cArray.mli | 16 +++++++++------- clib/cEphemeron.ml | 10 ++++++---- clib/cEphemeron.mli | 10 ++++++---- clib/cList.ml | 16 +++++++++------- clib/cList.mli | 16 +++++++++------- clib/cMap.ml | 10 ++++++---- clib/cMap.mli | 10 ++++++---- clib/cObj.ml | 16 +++++++++------- clib/cObj.mli | 16 +++++++++------- clib/cSet.ml | 10 ++++++---- clib/cSet.mli | 10 ++++++---- clib/cSig.mli | 10 ++++++---- clib/cStack.ml | 10 ++++++---- clib/cStack.mli | 10 ++++++---- clib/cString.ml | 10 ++++++---- clib/cString.mli | 10 ++++++---- clib/cThread.ml | 10 ++++++---- clib/cThread.mli | 10 ++++++---- clib/cUnix.ml | 10 ++++++---- clib/cUnix.mli | 10 ++++++---- clib/canary.ml | 10 ++++++---- clib/canary.mli | 10 ++++++---- clib/deque.ml | 10 ++++++---- clib/deque.mli | 10 ++++++---- clib/dyn.ml | 10 ++++++---- clib/dyn.mli | 10 ++++++---- clib/exninfo.ml | 16 +++++++++------- clib/exninfo.mli | 16 +++++++++------- clib/hMap.ml | 10 ++++++---- clib/hMap.mli | 10 ++++++---- clib/hashcons.ml | 10 ++++++---- clib/hashcons.mli | 10 ++++++---- clib/hashset.ml | 10 ++++++---- clib/hashset.mli | 10 ++++++---- clib/heap.ml | 10 ++++++---- clib/heap.mli | 10 ++++++---- clib/iStream.ml | 10 ++++++---- clib/iStream.mli | 10 ++++++---- clib/int.ml | 10 ++++++---- clib/int.mli | 10 ++++++---- clib/minisys.ml | 10 ++++++---- clib/monad.ml | 16 +++++++++------- clib/monad.mli | 16 +++++++++------- clib/option.ml | 10 ++++++---- clib/option.mli | 10 ++++++---- clib/range.ml | 10 ++++++---- clib/range.mli | 10 ++++++---- clib/segmenttree.ml | 10 ++++++---- clib/segmenttree.mli | 10 ++++++---- clib/store.ml | 16 +++++++++------- clib/store.mli | 16 +++++++++------- clib/terminal.ml | 10 ++++++---- clib/terminal.mli | 10 ++++++---- clib/trie.ml | 10 ++++++---- clib/trie.mli | 10 ++++++---- clib/unicode.ml | 16 +++++++++------- clib/unicode.mli | 10 ++++++---- clib/unionfind.ml | 10 ++++++---- clib/unionfind.mli | 10 ++++++---- config/coq_config.mli | 10 ++++++---- dev/top_printers.ml | 10 ++++++---- dev/top_printers.mli | 10 ++++++---- engine/eConstr.ml | 10 ++++++---- engine/eConstr.mli | 10 ++++++---- engine/evarutil.ml | 10 ++++++---- engine/evarutil.mli | 10 ++++++---- engine/evd.ml | 10 ++++++---- engine/evd.mli | 10 ++++++---- engine/ftactic.ml | 10 ++++++---- engine/ftactic.mli | 10 ++++++---- engine/logic_monad.ml | 10 ++++++---- engine/logic_monad.mli | 10 ++++++---- engine/namegen.ml | 10 ++++++---- engine/namegen.mli | 10 ++++++---- engine/nameops.ml | 10 ++++++---- engine/nameops.mli | 10 ++++++---- engine/proofview.ml | 10 ++++++---- engine/proofview.mli | 10 ++++++---- engine/proofview_monad.ml | 10 ++++++---- engine/proofview_monad.mli | 10 ++++++---- engine/termops.ml | 10 ++++++---- engine/termops.mli | 10 ++++++---- engine/uState.ml | 10 ++++++---- engine/uState.mli | 10 ++++++---- engine/universes.ml | 10 ++++++---- engine/universes.mli | 10 ++++++---- engine/univops.ml | 10 ++++++---- engine/univops.mli | 10 ++++++---- grammar/argextend.mlp | 10 ++++++---- grammar/q_util.mli | 10 ++++++---- grammar/q_util.mlp | 10 ++++++---- grammar/tacextend.mlp | 10 ++++++---- grammar/vernacextend.mlp | 10 ++++++---- ide/config_lexer.mli | 10 ++++++---- ide/config_lexer.mll | 10 ++++++---- ide/coq.ml | 10 ++++++---- ide/coq.mli | 10 ++++++---- ide/coqOps.ml | 10 ++++++---- ide/coqOps.mli | 10 ++++++---- ide/coq_commands.ml | 10 ++++++---- ide/coq_commands.mli | 10 ++++++---- ide/coq_lex.mli | 10 ++++++---- ide/coq_lex.mll | 10 ++++++---- ide/coqide.ml | 10 ++++++---- ide/coqide.mli | 10 ++++++---- ide/coqide_main.ml4 | 10 ++++++---- ide/coqide_main.mli | 10 ++++++---- ide/coqide_ui.mli | 10 ++++++---- ide/document.ml | 10 ++++++---- ide/document.mli | 10 ++++++---- ide/fileOps.ml | 10 ++++++---- ide/fileOps.mli | 10 ++++++---- ide/gtk_parsing.ml | 10 ++++++---- ide/gtk_parsing.mli | 10 ++++++---- ide/ide_slave.ml | 10 ++++++---- ide/ide_slave.mli | 10 ++++++---- ide/ideutils.ml | 10 ++++++---- ide/ideutils.mli | 10 ++++++---- ide/interface.mli | 10 ++++++---- ide/macos_prehook.mli | 10 ++++++---- ide/minilib.ml | 16 +++++++++------- ide/minilib.mli | 16 +++++++++------- ide/nanoPG.ml | 10 ++++++---- ide/nanoPG.mli | 10 ++++++---- ide/preferences.ml | 10 ++++++---- ide/preferences.mli | 10 ++++++---- ide/richpp.ml | 10 ++++++---- ide/richpp.mli | 10 ++++++---- ide/sentence.ml | 10 ++++++---- ide/sentence.mli | 10 ++++++---- ide/serialize.ml | 10 ++++++---- ide/serialize.mli | 10 ++++++---- ide/session.ml | 10 ++++++---- ide/session.mli | 10 ++++++---- ide/tags.ml | 10 ++++++---- ide/tags.mli | 10 ++++++---- ide/utf8_convert.mli | 10 ++++++---- ide/utf8_convert.mll | 10 ++++++---- ide/wg_Command.ml | 10 ++++++---- ide/wg_Command.mli | 10 ++++++---- ide/wg_Completion.ml | 10 ++++++---- ide/wg_Completion.mli | 10 ++++++---- ide/wg_Detachable.ml | 10 ++++++---- ide/wg_Detachable.mli | 10 ++++++---- ide/wg_Find.ml | 10 ++++++---- ide/wg_Find.mli | 10 ++++++---- ide/wg_MessageView.ml | 10 ++++++---- ide/wg_MessageView.mli | 10 ++++++---- ide/wg_Notebook.ml | 10 ++++++---- ide/wg_Notebook.mli | 10 ++++++---- ide/wg_ProofView.ml | 10 ++++++---- ide/wg_ProofView.mli | 10 ++++++---- ide/wg_ScriptView.ml | 10 ++++++---- ide/wg_ScriptView.mli | 10 ++++++---- ide/wg_Segment.ml | 10 ++++++---- ide/wg_Segment.mli | 10 ++++++---- ide/xml_printer.ml | 10 ++++++---- ide/xml_printer.mli | 10 ++++++---- ide/xmlprotocol.ml | 10 ++++++---- ide/xmlprotocol.mli | 10 ++++++---- interp/constrexpr_ops.ml | 10 ++++++---- interp/constrexpr_ops.mli | 10 ++++++---- interp/constrextern.ml | 10 ++++++---- interp/constrextern.mli | 10 ++++++---- interp/constrintern.ml | 10 ++++++---- interp/constrintern.mli | 10 ++++++---- interp/declare.ml | 10 ++++++---- interp/declare.mli | 10 ++++++---- interp/discharge.ml | 10 ++++++---- interp/discharge.mli | 10 ++++++---- interp/dumpglob.ml | 10 ++++++---- interp/dumpglob.mli | 10 ++++++---- interp/genintern.ml | 10 ++++++---- interp/genintern.mli | 10 ++++++---- interp/impargs.ml | 10 ++++++---- interp/impargs.mli | 10 ++++++---- interp/implicit_quantifiers.ml | 10 ++++++---- interp/implicit_quantifiers.mli | 10 ++++++---- interp/modintern.ml | 10 ++++++---- interp/modintern.mli | 10 ++++++---- interp/notation.ml | 10 ++++++---- interp/notation.mli | 10 ++++++---- interp/notation_ops.ml | 10 ++++++---- interp/notation_ops.mli | 10 ++++++---- interp/ppextend.ml | 10 ++++++---- interp/ppextend.mli | 10 ++++++---- interp/reserve.ml | 10 ++++++---- interp/reserve.mli | 10 ++++++---- interp/smartlocate.ml | 10 ++++++---- interp/smartlocate.mli | 10 ++++++---- interp/stdarg.ml | 10 ++++++---- interp/stdarg.mli | 10 ++++++---- interp/syntax_def.ml | 10 ++++++---- interp/syntax_def.mli | 10 ++++++---- interp/tactypes.ml | 10 ++++++---- interp/topconstr.ml | 10 ++++++---- interp/topconstr.mli | 10 ++++++---- intf/constrexpr.ml | 10 ++++++---- intf/decl_kinds.ml | 10 ++++++---- intf/evar_kinds.ml | 10 ++++++---- intf/extend.ml | 10 ++++++---- intf/genredexpr.ml | 10 ++++++---- intf/glob_term.ml | 10 ++++++---- intf/locus.ml | 10 ++++++---- intf/misctypes.ml | 10 ++++++---- intf/notation_term.ml | 10 ++++++---- intf/pattern.ml | 10 ++++++---- intf/vernacexpr.ml | 10 ++++++---- kernel/cClosure.ml | 10 ++++++---- kernel/cClosure.mli | 10 ++++++---- kernel/cPrimitives.ml | 10 ++++++---- kernel/cPrimitives.mli | 10 ++++++---- kernel/cbytecodes.ml | 10 ++++++---- kernel/cbytecodes.mli | 10 ++++++---- kernel/cbytegen.ml | 10 ++++++---- kernel/cbytegen.mli | 10 ++++++---- kernel/cemitcodes.ml | 10 ++++++---- kernel/cinstr.mli | 10 ++++++---- kernel/constr.ml | 10 ++++++---- kernel/constr.mli | 10 ++++++---- kernel/context.ml | 10 ++++++---- kernel/context.mli | 10 ++++++---- kernel/conv_oracle.ml | 10 ++++++---- kernel/conv_oracle.mli | 10 ++++++---- kernel/cooking.ml | 10 ++++++---- kernel/cooking.mli | 10 ++++++---- kernel/csymtable.ml | 10 ++++++---- kernel/csymtable.mli | 10 ++++++---- kernel/declarations.ml | 10 ++++++---- kernel/declareops.ml | 10 ++++++---- kernel/declareops.mli | 10 ++++++---- kernel/entries.ml | 10 ++++++---- kernel/environ.ml | 10 ++++++---- kernel/environ.mli | 10 ++++++---- kernel/esubst.ml | 10 ++++++---- kernel/esubst.mli | 10 ++++++---- kernel/evar.ml | 10 ++++++---- kernel/evar.mli | 10 ++++++---- kernel/indtypes.ml | 10 ++++++---- kernel/indtypes.mli | 10 ++++++---- kernel/inductive.ml | 10 ++++++---- kernel/inductive.mli | 10 ++++++---- kernel/mod_subst.ml | 10 ++++++---- kernel/mod_subst.mli | 10 ++++++---- kernel/mod_typing.ml | 10 ++++++---- kernel/mod_typing.mli | 10 ++++++---- kernel/modops.ml | 10 ++++++---- kernel/modops.mli | 10 ++++++---- kernel/names.ml | 10 ++++++---- kernel/names.mli | 10 ++++++---- kernel/nativecode.ml | 10 ++++++---- kernel/nativecode.mli | 10 ++++++---- kernel/nativeconv.ml | 10 ++++++---- kernel/nativeconv.mli | 10 ++++++---- kernel/nativeinstr.mli | 10 ++++++---- kernel/nativelambda.ml | 10 ++++++---- kernel/nativelambda.mli | 10 ++++++---- kernel/nativelib.ml | 10 ++++++---- kernel/nativelib.mli | 10 ++++++---- kernel/nativelibrary.ml | 10 ++++++---- kernel/nativelibrary.mli | 10 ++++++---- kernel/nativevalues.ml | 10 ++++++---- kernel/nativevalues.mli | 10 ++++++---- kernel/opaqueproof.ml | 10 ++++++---- kernel/opaqueproof.mli | 10 ++++++---- kernel/pre_env.ml | 10 ++++++---- kernel/pre_env.mli | 10 ++++++---- kernel/reduction.ml | 10 ++++++---- kernel/reduction.mli | 10 ++++++---- kernel/retroknowledge.ml | 10 ++++++---- kernel/retroknowledge.mli | 10 ++++++---- kernel/safe_typing.ml | 10 ++++++---- kernel/safe_typing.mli | 10 ++++++---- kernel/sorts.ml | 10 ++++++---- kernel/sorts.mli | 10 ++++++---- kernel/subtyping.ml | 10 ++++++---- kernel/subtyping.mli | 10 ++++++---- kernel/term.ml | 10 ++++++---- kernel/term.mli | 10 ++++++---- kernel/term_typing.ml | 10 ++++++---- kernel/term_typing.mli | 10 ++++++---- kernel/type_errors.ml | 10 ++++++---- kernel/type_errors.mli | 10 ++++++---- kernel/typeops.ml | 10 ++++++---- kernel/typeops.mli | 10 ++++++---- kernel/uGraph.ml | 10 ++++++---- kernel/uGraph.mli | 10 ++++++---- kernel/univ.ml | 10 ++++++---- kernel/univ.mli | 10 ++++++---- kernel/vars.ml | 10 ++++++---- kernel/vars.mli | 10 ++++++---- kernel/vconv.mli | 10 ++++++---- kernel/vm.ml | 10 ++++++---- kernel/vm.mli | 10 ++++++---- kernel/vmvalues.ml | 10 ++++++---- kernel/vmvalues.mli | 10 ++++++---- lib/aux_file.ml | 10 ++++++---- lib/aux_file.mli | 10 ++++++---- lib/cAst.ml | 10 ++++++---- lib/cAst.mli | 10 ++++++---- lib/cErrors.ml | 16 +++++++++------- lib/cErrors.mli | 16 +++++++++------- lib/cProfile.ml | 10 ++++++---- lib/cProfile.mli | 10 ++++++---- lib/cWarnings.ml | 10 ++++++---- lib/cWarnings.mli | 10 ++++++---- lib/control.ml | 10 ++++++---- lib/control.mli | 10 ++++++---- lib/coqProject_file.ml4 | 10 ++++++---- lib/coqProject_file.mli | 10 ++++++---- lib/dAst.ml | 10 ++++++---- lib/dAst.mli | 10 ++++++---- lib/envars.ml | 10 ++++++---- lib/envars.mli | 10 ++++++---- lib/explore.ml | 10 ++++++---- lib/explore.mli | 10 ++++++---- lib/feedback.ml | 10 ++++++---- lib/feedback.mli | 10 ++++++---- lib/flags.ml | 10 ++++++---- lib/flags.mli | 10 ++++++---- lib/future.ml | 10 ++++++---- lib/future.mli | 10 ++++++---- lib/genarg.ml | 10 ++++++---- lib/genarg.mli | 10 ++++++---- lib/hook.ml | 10 ++++++---- lib/hook.mli | 10 ++++++---- lib/loc.ml | 10 ++++++---- lib/loc.mli | 10 ++++++---- lib/pp.ml | 10 ++++++---- lib/pp.mli | 10 ++++++---- lib/remoteCounter.ml | 10 ++++++---- lib/remoteCounter.mli | 10 ++++++---- lib/rtree.ml | 10 ++++++---- lib/rtree.mli | 10 ++++++---- lib/spawn.ml | 10 ++++++---- lib/spawn.mli | 10 ++++++---- lib/stateid.ml | 10 ++++++---- lib/stateid.mli | 10 ++++++---- lib/system.ml | 10 ++++++---- lib/system.mli | 10 ++++++---- lib/util.ml | 16 +++++++++------- lib/util.mli | 10 ++++++---- lib/xml_datatype.mli | 10 ++++++---- library/coqlib.ml | 10 ++++++---- library/coqlib.mli | 10 ++++++---- library/declaremods.ml | 10 ++++++---- library/declaremods.mli | 10 ++++++---- library/decls.ml | 10 ++++++---- library/decls.mli | 10 ++++++---- library/dischargedhypsmap.ml | 10 ++++++---- library/dischargedhypsmap.mli | 10 ++++++---- library/global.ml | 10 ++++++---- library/global.mli | 10 ++++++---- library/globnames.ml | 10 ++++++---- library/globnames.mli | 10 ++++++---- library/goptions.ml | 10 ++++++---- library/goptions.mli | 10 ++++++---- library/heads.ml | 10 ++++++---- library/heads.mli | 10 ++++++---- library/keys.ml | 10 ++++++---- library/keys.mli | 10 ++++++---- library/kindops.ml | 10 ++++++---- library/kindops.mli | 10 ++++++---- library/lib.ml | 10 ++++++---- library/lib.mli | 10 ++++++---- library/libnames.ml | 10 ++++++---- library/libnames.mli | 10 ++++++---- library/libobject.ml | 10 ++++++---- library/libobject.mli | 10 ++++++---- library/library.ml | 10 ++++++---- library/library.mli | 10 ++++++---- library/loadpath.ml | 10 ++++++---- library/loadpath.mli | 10 ++++++---- library/nametab.ml | 10 ++++++---- library/nametab.mli | 10 ++++++---- library/states.ml | 10 ++++++---- library/states.mli | 10 ++++++---- library/summary.ml | 10 ++++++---- library/summary.mli | 10 ++++++---- parsing/cLexer.ml4 | 10 ++++++---- parsing/cLexer.mli | 10 ++++++---- parsing/egramcoq.ml | 10 ++++++---- parsing/egramcoq.mli | 10 ++++++---- parsing/egramml.ml | 10 ++++++---- parsing/egramml.mli | 10 ++++++---- parsing/g_constr.ml4 | 10 ++++++---- parsing/g_prim.ml4 | 10 ++++++---- parsing/g_proofs.ml4 | 10 ++++++---- parsing/g_vernac.ml4 | 10 ++++++---- parsing/pcoq.ml | 10 ++++++---- parsing/pcoq.mli | 10 ++++++---- parsing/tok.ml | 10 ++++++---- parsing/tok.mli | 10 ++++++---- plugins/btauto/g_btauto.ml4 | 10 ++++++---- plugins/cc/ccalgo.ml | 10 ++++++---- plugins/cc/ccalgo.mli | 10 ++++++---- plugins/cc/ccproof.ml | 10 ++++++---- plugins/cc/ccproof.mli | 10 ++++++---- plugins/cc/cctac.ml | 10 ++++++---- plugins/cc/cctac.mli | 11 ++++++----- plugins/cc/g_congruence.ml4 | 10 ++++++---- plugins/derive/derive.ml | 10 ++++++---- plugins/derive/derive.mli | 10 ++++++---- plugins/derive/g_derive.ml4 | 10 ++++++---- plugins/extraction/ExtrOcamlBasic.v | 10 ++++++---- plugins/extraction/ExtrOcamlBigIntConv.v | 10 ++++++---- plugins/extraction/ExtrOcamlIntConv.v | 10 ++++++---- plugins/extraction/ExtrOcamlNatBigInt.v | 10 ++++++---- plugins/extraction/ExtrOcamlNatInt.v | 10 ++++++---- plugins/extraction/ExtrOcamlString.v | 10 ++++++---- plugins/extraction/ExtrOcamlZBigInt.v | 10 ++++++---- plugins/extraction/ExtrOcamlZInt.v | 10 ++++++---- plugins/extraction/Extraction.v | 10 ++++++---- plugins/extraction/big.ml | 10 ++++++---- plugins/extraction/common.ml | 10 ++++++---- plugins/extraction/common.mli | 10 ++++++---- plugins/extraction/extract_env.ml | 10 ++++++---- plugins/extraction/extract_env.mli | 10 ++++++---- plugins/extraction/extraction.ml | 10 ++++++---- plugins/extraction/extraction.mli | 10 ++++++---- plugins/extraction/g_extraction.ml4 | 10 ++++++---- plugins/extraction/haskell.ml | 10 ++++++---- plugins/extraction/haskell.mli | 10 ++++++---- plugins/extraction/miniml.mli | 10 ++++++---- plugins/extraction/mlutil.ml | 10 ++++++---- plugins/extraction/mlutil.mli | 10 ++++++---- plugins/extraction/modutil.ml | 10 ++++++---- plugins/extraction/modutil.mli | 10 ++++++---- plugins/extraction/ocaml.ml | 10 ++++++---- plugins/extraction/ocaml.mli | 10 ++++++---- plugins/extraction/scheme.ml | 10 ++++++---- plugins/extraction/scheme.mli | 10 ++++++---- plugins/extraction/table.ml | 10 ++++++---- plugins/extraction/table.mli | 10 ++++++---- plugins/firstorder/formula.ml | 10 ++++++---- plugins/firstorder/formula.mli | 10 ++++++---- plugins/firstorder/g_ground.ml4 | 10 ++++++---- plugins/firstorder/ground.ml | 10 ++++++---- plugins/firstorder/ground.mli | 10 ++++++---- plugins/firstorder/instances.ml | 10 ++++++---- plugins/firstorder/instances.mli | 10 ++++++---- plugins/firstorder/rules.ml | 10 ++++++---- plugins/firstorder/rules.mli | 10 ++++++---- plugins/firstorder/sequent.ml | 10 ++++++---- plugins/firstorder/sequent.mli | 10 ++++++---- plugins/firstorder/unify.ml | 10 ++++++---- plugins/firstorder/unify.mli | 10 ++++++---- plugins/fourier/Fourier.v | 10 ++++++---- plugins/fourier/Fourier_util.v | 10 ++++++---- plugins/fourier/fourier.ml | 10 ++++++---- plugins/fourier/fourierR.ml | 10 ++++++---- plugins/fourier/g_fourier.ml4 | 10 ++++++---- plugins/funind/FunInd.v | 10 ++++++---- plugins/funind/Recdef.v | 10 ++++++---- plugins/funind/functional_principles_types.mli | 10 ++++++---- plugins/funind/g_indfun.ml4 | 10 ++++++---- plugins/funind/invfun.ml | 10 ++++++---- plugins/funind/invfun.mli | 10 ++++++---- plugins/funind/recdef.ml | 10 ++++++---- plugins/ltac/coretactics.ml4 | 10 ++++++---- plugins/ltac/evar_tactics.ml | 10 ++++++---- plugins/ltac/evar_tactics.mli | 10 ++++++---- plugins/ltac/extraargs.ml4 | 10 ++++++---- plugins/ltac/extraargs.mli | 10 ++++++---- plugins/ltac/extratactics.ml4 | 10 ++++++---- plugins/ltac/extratactics.mli | 10 ++++++---- plugins/ltac/g_auto.ml4 | 10 ++++++---- plugins/ltac/g_class.ml4 | 10 ++++++---- plugins/ltac/g_eqdecide.ml4 | 10 ++++++---- plugins/ltac/g_ltac.ml4 | 10 ++++++---- plugins/ltac/g_obligations.ml4 | 10 ++++++---- plugins/ltac/g_rewrite.ml4 | 10 ++++++---- plugins/ltac/g_tactic.ml4 | 10 ++++++---- plugins/ltac/pltac.ml | 10 ++++++---- plugins/ltac/pltac.mli | 10 ++++++---- plugins/ltac/pptactic.ml | 10 ++++++---- plugins/ltac/pptactic.mli | 10 ++++++---- plugins/ltac/profile_ltac.ml | 10 ++++++---- plugins/ltac/profile_ltac.mli | 10 ++++++---- plugins/ltac/profile_ltac_tactics.ml4 | 10 ++++++---- plugins/ltac/rewrite.ml | 10 ++++++---- plugins/ltac/rewrite.mli | 10 ++++++---- plugins/ltac/tacarg.ml | 10 ++++++---- plugins/ltac/tacarg.mli | 10 ++++++---- plugins/ltac/taccoerce.ml | 10 ++++++---- plugins/ltac/taccoerce.mli | 10 ++++++---- plugins/ltac/tacentries.ml | 10 ++++++---- plugins/ltac/tacentries.mli | 10 ++++++---- plugins/ltac/tacenv.ml | 10 ++++++---- plugins/ltac/tacenv.mli | 10 ++++++---- plugins/ltac/tacexpr.mli | 10 ++++++---- plugins/ltac/tacintern.ml | 10 ++++++---- plugins/ltac/tacintern.mli | 10 ++++++---- plugins/ltac/tacinterp.ml | 10 ++++++---- plugins/ltac/tacinterp.mli | 10 ++++++---- plugins/ltac/tacsubst.ml | 10 ++++++---- plugins/ltac/tacsubst.mli | 10 ++++++---- plugins/ltac/tactic_debug.ml | 10 ++++++---- plugins/ltac/tactic_debug.mli | 10 ++++++---- plugins/ltac/tactic_matching.ml | 10 ++++++---- plugins/ltac/tactic_matching.mli | 12 +++++++----- plugins/ltac/tactic_option.ml | 10 ++++++---- plugins/ltac/tactic_option.mli | 10 ++++++---- plugins/ltac/tauto.ml | 10 ++++++---- plugins/micromega/Env.v | 10 ++++++---- plugins/micromega/EnvRing.v | 10 ++++++---- plugins/micromega/Lia.v | 10 ++++++---- plugins/micromega/Lqa.v | 10 ++++++---- plugins/micromega/Lra.v | 10 ++++++---- plugins/micromega/MExtraction.v | 10 ++++++---- plugins/micromega/OrderedRing.v | 10 ++++++---- plugins/micromega/Psatz.v | 10 ++++++---- plugins/micromega/QMicromega.v | 10 ++++++---- plugins/micromega/RMicromega.v | 10 ++++++---- plugins/micromega/Refl.v | 10 ++++++---- plugins/micromega/RingMicromega.v | 10 ++++++---- plugins/micromega/Tauto.v | 10 ++++++---- plugins/micromega/ZCoeff.v | 10 ++++++---- plugins/micromega/ZMicromega.v | 10 ++++++---- plugins/micromega/certificate.ml | 10 ++++++---- plugins/micromega/coq_micromega.ml | 10 ++++++---- plugins/micromega/csdpcert.ml | 10 ++++++---- plugins/micromega/g_micromega.ml4 | 10 ++++++---- plugins/micromega/mutils.ml | 10 ++++++---- plugins/micromega/persistent_cache.ml | 10 ++++++---- plugins/micromega/polynomial.ml | 10 ++++++---- plugins/micromega/sos.mli | 10 ++++++---- plugins/micromega/sos_types.ml | 10 ++++++---- plugins/micromega/sos_types.mli | 10 ++++++---- plugins/nsatz/Nsatz.v | 10 ++++++---- plugins/nsatz/g_nsatz.ml4 | 10 ++++++---- plugins/nsatz/ideal.ml | 10 ++++++---- plugins/nsatz/ideal.mli | 10 ++++++---- plugins/nsatz/nsatz.ml | 10 ++++++---- plugins/nsatz/nsatz.mli | 10 ++++++---- plugins/nsatz/polynom.ml | 10 ++++++---- plugins/nsatz/polynom.mli | 10 ++++++---- plugins/omega/Omega.v | 10 ++++++---- plugins/omega/OmegaLemmas.v | 16 +++++++++------- plugins/omega/OmegaPlugin.v | 10 ++++++---- plugins/omega/OmegaTactic.v | 10 ++++++---- plugins/omega/PreOmega.v | 10 ++++++---- plugins/omega/coq_omega.ml | 10 ++++++---- plugins/omega/g_omega.ml4 | 10 ++++++---- plugins/omega/omega.ml | 10 ++++++---- plugins/quote/Quote.v | 10 ++++++---- plugins/quote/g_quote.ml4 | 10 ++++++---- plugins/quote/quote.ml | 10 ++++++---- plugins/rtauto/Bintree.v | 10 ++++++---- plugins/rtauto/Rtauto.v | 10 ++++++---- plugins/rtauto/g_rtauto.ml4 | 10 ++++++---- plugins/rtauto/proof_search.ml | 10 ++++++---- plugins/rtauto/proof_search.mli | 10 ++++++---- plugins/rtauto/refl_tauto.ml | 10 ++++++---- plugins/rtauto/refl_tauto.mli | 10 ++++++---- plugins/setoid_ring/ArithRing.v | 10 ++++++---- plugins/setoid_ring/BinList.v | 10 ++++++---- plugins/setoid_ring/Cring.v | 10 ++++++---- plugins/setoid_ring/Field.v | 10 ++++++---- plugins/setoid_ring/Field_tac.v | 10 ++++++---- plugins/setoid_ring/Field_theory.v | 10 ++++++---- plugins/setoid_ring/InitialRing.v | 10 ++++++---- plugins/setoid_ring/NArithRing.v | 10 ++++++---- plugins/setoid_ring/Ncring.v | 10 ++++++---- plugins/setoid_ring/Ncring_initial.v | 10 ++++++---- plugins/setoid_ring/Ncring_polynom.v | 10 ++++++---- plugins/setoid_ring/Ncring_tac.v | 10 ++++++---- plugins/setoid_ring/Ring.v | 10 ++++++---- plugins/setoid_ring/Ring_base.v | 10 ++++++---- plugins/setoid_ring/Ring_polynom.v | 10 ++++++---- plugins/setoid_ring/Ring_theory.v | 10 ++++++---- plugins/setoid_ring/ZArithRing.v | 10 ++++++---- plugins/setoid_ring/g_newring.ml4 | 10 ++++++---- plugins/setoid_ring/newring.ml | 10 ++++++---- plugins/setoid_ring/newring.mli | 10 ++++++---- plugins/setoid_ring/newring_ast.mli | 10 ++++++---- plugins/ssr/ssrast.mli | 10 ++++++---- plugins/ssr/ssrbool.v | 10 ++++++---- plugins/ssr/ssrbwd.ml | 10 ++++++---- plugins/ssr/ssrbwd.mli | 10 ++++++---- plugins/ssr/ssrcommon.ml | 10 ++++++---- plugins/ssr/ssrcommon.mli | 10 ++++++---- plugins/ssr/ssreflect.v | 10 ++++++---- plugins/ssr/ssrelim.ml | 10 ++++++---- plugins/ssr/ssrelim.mli | 10 ++++++---- plugins/ssr/ssrequality.ml | 10 ++++++---- plugins/ssr/ssrequality.mli | 10 ++++++---- plugins/ssr/ssrfun.v | 10 ++++++---- plugins/ssr/ssrfwd.ml | 10 ++++++---- plugins/ssr/ssrfwd.mli | 10 ++++++---- plugins/ssr/ssripats.ml | 10 ++++++---- plugins/ssr/ssripats.mli | 10 ++++++---- plugins/ssr/ssrparser.ml4 | 10 ++++++---- plugins/ssr/ssrparser.mli | 10 ++++++---- plugins/ssr/ssrprinters.ml | 10 ++++++---- plugins/ssr/ssrprinters.mli | 10 ++++++---- plugins/ssr/ssrtacticals.ml | 10 ++++++---- plugins/ssr/ssrtacticals.mli | 10 ++++++---- plugins/ssr/ssrvernac.ml4 | 10 ++++++---- plugins/ssr/ssrvernac.mli | 10 ++++++---- plugins/ssr/ssrview.ml | 10 ++++++---- plugins/ssr/ssrview.mli | 10 ++++++---- plugins/ssrmatching/ssrmatching.ml4 | 10 ++++++---- plugins/syntax/ascii_syntax.ml | 16 +++++++++------- plugins/syntax/int31_syntax.ml | 10 ++++++---- plugins/syntax/nat_syntax.ml | 10 ++++++---- plugins/syntax/r_syntax.ml | 10 ++++++---- plugins/syntax/string_syntax.ml | 16 +++++++++------- plugins/syntax/z_syntax.ml | 10 ++++++---- pretyping/arguments_renaming.ml | 10 ++++++---- pretyping/arguments_renaming.mli | 10 ++++++---- pretyping/cases.ml | 10 ++++++---- pretyping/cases.mli | 10 ++++++---- pretyping/cbv.ml | 10 ++++++---- pretyping/cbv.mli | 10 ++++++---- pretyping/classops.ml | 10 ++++++---- pretyping/classops.mli | 10 ++++++---- pretyping/coercion.ml | 10 ++++++---- pretyping/coercion.mli | 10 ++++++---- pretyping/constr_matching.ml | 10 ++++++---- pretyping/constr_matching.mli | 10 ++++++---- pretyping/detyping.ml | 10 ++++++---- pretyping/detyping.mli | 10 ++++++---- pretyping/evarconv.ml | 10 ++++++---- pretyping/evarconv.mli | 10 ++++++---- pretyping/evardefine.ml | 10 ++++++---- pretyping/evardefine.mli | 10 ++++++---- pretyping/evarsolve.ml | 10 ++++++---- pretyping/evarsolve.mli | 10 ++++++---- pretyping/find_subterm.ml | 10 ++++++---- pretyping/find_subterm.mli | 10 ++++++---- pretyping/geninterp.ml | 10 ++++++---- pretyping/geninterp.mli | 10 ++++++---- pretyping/glob_ops.ml | 10 ++++++---- pretyping/glob_ops.mli | 10 ++++++---- pretyping/indrec.ml | 10 ++++++---- pretyping/indrec.mli | 10 ++++++---- pretyping/inductiveops.ml | 10 ++++++---- pretyping/inductiveops.mli | 10 ++++++---- pretyping/inferCumulativity.ml | 10 ++++++---- pretyping/inferCumulativity.mli | 10 ++++++---- pretyping/locusops.ml | 10 ++++++---- pretyping/locusops.mli | 10 ++++++---- pretyping/miscops.ml | 10 ++++++---- pretyping/miscops.mli | 10 ++++++---- pretyping/nativenorm.ml | 10 ++++++---- pretyping/nativenorm.mli | 10 ++++++---- pretyping/patternops.ml | 10 ++++++---- pretyping/patternops.mli | 10 ++++++---- pretyping/pretype_errors.ml | 10 ++++++---- pretyping/pretype_errors.mli | 10 ++++++---- pretyping/pretyping.ml | 10 ++++++---- pretyping/pretyping.mli | 10 ++++++---- pretyping/program.ml | 10 ++++++---- pretyping/program.mli | 10 ++++++---- pretyping/recordops.ml | 10 ++++++---- pretyping/recordops.mli | 10 ++++++---- pretyping/redops.ml | 10 ++++++---- pretyping/redops.mli | 10 ++++++---- pretyping/reductionops.ml | 10 ++++++---- pretyping/reductionops.mli | 10 ++++++---- pretyping/retyping.ml | 10 ++++++---- pretyping/retyping.mli | 10 ++++++---- pretyping/tacred.ml | 10 ++++++---- pretyping/tacred.mli | 10 ++++++---- pretyping/typeclasses.ml | 10 ++++++---- pretyping/typeclasses.mli | 10 ++++++---- pretyping/typeclasses_errors.ml | 10 ++++++---- pretyping/typeclasses_errors.mli | 10 ++++++---- pretyping/typing.ml | 10 ++++++---- pretyping/typing.mli | 10 ++++++---- pretyping/unification.ml | 10 ++++++---- pretyping/unification.mli | 10 ++++++---- pretyping/univdecls.ml | 10 ++++++---- pretyping/univdecls.mli | 10 ++++++---- pretyping/vnorm.ml | 10 ++++++---- pretyping/vnorm.mli | 10 ++++++---- printing/genprint.ml | 10 ++++++---- printing/genprint.mli | 10 ++++++---- printing/ppconstr.ml | 10 ++++++---- printing/ppconstr.mli | 10 ++++++---- printing/pputils.ml | 10 ++++++---- printing/pputils.mli | 10 ++++++---- printing/ppvernac.ml | 10 ++++++---- printing/ppvernac.mli | 10 ++++++---- printing/prettyp.ml | 10 ++++++---- printing/prettyp.mli | 10 ++++++---- printing/printer.ml | 10 ++++++---- printing/printer.mli | 10 ++++++---- printing/printmod.ml | 10 ++++++---- printing/printmod.mli | 10 ++++++---- proofs/clenv.ml | 10 ++++++---- proofs/clenv.mli | 10 ++++++---- proofs/clenvtac.ml | 10 ++++++---- proofs/clenvtac.mli | 10 ++++++---- proofs/evar_refiner.ml | 10 ++++++---- proofs/evar_refiner.mli | 10 ++++++---- proofs/goal.ml | 10 ++++++---- proofs/goal.mli | 10 ++++++---- proofs/logic.ml | 10 ++++++---- proofs/logic.mli | 10 ++++++---- proofs/miscprint.ml | 10 ++++++---- proofs/miscprint.mli | 10 ++++++---- proofs/pfedit.ml | 10 ++++++---- proofs/pfedit.mli | 10 ++++++---- proofs/proof.ml | 10 ++++++---- proofs/proof.mli | 10 ++++++---- proofs/proof_bullet.ml | 10 ++++++---- proofs/proof_bullet.mli | 10 ++++++---- proofs/proof_global.ml | 10 ++++++---- proofs/proof_global.mli | 10 ++++++---- proofs/proof_type.ml | 10 ++++++---- proofs/redexpr.ml | 10 ++++++---- proofs/redexpr.mli | 10 ++++++---- proofs/refine.ml | 10 ++++++---- proofs/refine.mli | 10 ++++++---- proofs/refiner.ml | 10 ++++++---- proofs/refiner.mli | 10 ++++++---- proofs/tacmach.ml | 10 ++++++---- proofs/tacmach.mli | 10 ++++++---- stm/asyncTaskQueue.ml | 10 ++++++---- stm/asyncTaskQueue.mli | 10 ++++++---- stm/coqworkmgrApi.ml | 10 ++++++---- stm/coqworkmgrApi.mli | 10 ++++++---- stm/dag.ml | 10 ++++++---- stm/dag.mli | 10 ++++++---- stm/proofBlockDelimiter.ml | 10 ++++++---- stm/proofBlockDelimiter.mli | 10 ++++++---- stm/proofworkertop.ml | 10 ++++++---- stm/queryworkertop.ml | 10 ++++++---- stm/spawned.ml | 10 ++++++---- stm/spawned.mli | 10 ++++++---- stm/stm.ml | 10 ++++++---- stm/stm.mli | 10 ++++++---- stm/tQueue.ml | 10 ++++++---- stm/tQueue.mli | 10 ++++++---- stm/tacworkertop.ml | 10 ++++++---- stm/vcs.ml | 10 ++++++---- stm/vcs.mli | 10 ++++++---- stm/vernac_classifier.ml | 10 ++++++---- stm/vernac_classifier.mli | 10 ++++++---- stm/vio_checking.ml | 10 ++++++---- stm/vio_checking.mli | 10 ++++++---- stm/workerLoop.ml | 10 ++++++---- stm/workerLoop.mli | 10 ++++++---- stm/workerPool.ml | 10 ++++++---- stm/workerPool.mli | 10 ++++++---- tactics/auto.ml | 10 ++++++---- tactics/auto.mli | 10 ++++++---- tactics/autorewrite.ml | 10 ++++++---- tactics/autorewrite.mli | 10 ++++++---- tactics/btermdn.ml | 10 ++++++---- tactics/btermdn.mli | 10 ++++++---- tactics/class_tactics.ml | 10 ++++++---- tactics/class_tactics.mli | 10 ++++++---- tactics/contradiction.ml | 10 ++++++---- tactics/contradiction.mli | 10 ++++++---- tactics/dnet.ml | 10 ++++++---- tactics/dnet.mli | 10 ++++++---- tactics/eauto.ml | 10 ++++++---- tactics/eauto.mli | 10 ++++++---- tactics/elim.ml | 10 ++++++---- tactics/elim.mli | 10 ++++++---- tactics/elimschemes.ml | 10 ++++++---- tactics/elimschemes.mli | 10 ++++++---- tactics/eqdecide.ml | 10 ++++++---- tactics/eqdecide.mli | 10 ++++++---- tactics/eqschemes.ml | 10 ++++++---- tactics/eqschemes.mli | 10 ++++++---- tactics/equality.ml | 10 ++++++---- tactics/equality.mli | 10 ++++++---- tactics/hints.ml | 10 ++++++---- tactics/hints.mli | 10 ++++++---- tactics/hipattern.ml | 10 ++++++---- tactics/hipattern.mli | 10 ++++++---- tactics/ind_tables.ml | 10 ++++++---- tactics/ind_tables.mli | 10 ++++++---- tactics/inv.ml | 10 ++++++---- tactics/inv.mli | 10 ++++++---- tactics/leminv.ml | 10 ++++++---- tactics/leminv.mli | 10 ++++++---- tactics/tacticals.ml | 10 ++++++---- tactics/tacticals.mli | 10 ++++++---- tactics/tactics.ml | 10 ++++++---- tactics/tactics.mli | 10 ++++++---- tactics/term_dnet.ml | 10 ++++++---- tactics/term_dnet.mli | 10 ++++++---- test-suite/Makefile | 16 +++++++++------- test-suite/failure/Tauto.v | 10 ++++++---- test-suite/failure/clash_cons.v | 10 ++++++---- test-suite/failure/fixpoint1.v | 10 ++++++---- test-suite/failure/guard.v | 10 ++++++---- test-suite/failure/illtype1.v | 10 ++++++---- test-suite/failure/positivity.v | 10 ++++++---- test-suite/failure/redef.v | 10 ++++++---- test-suite/failure/search.v | 10 ++++++---- test-suite/ideal-features/Apply.v | 10 ++++++---- test-suite/success/Check.v | 10 ++++++---- test-suite/success/Field.v | 10 ++++++---- test-suite/success/Tauto.v | 10 ++++++---- test-suite/success/TestRefine.v | 10 ++++++---- test-suite/success/eauto.v | 10 ++++++---- test-suite/success/eqdecide.v | 10 ++++++---- test-suite/success/extraction.v | 10 ++++++---- test-suite/success/inds_type_sec.v | 10 ++++++---- test-suite/success/induct.v | 10 ++++++---- test-suite/success/mutual_ind.v | 10 ++++++---- test-suite/success/unfold.v | 10 ++++++---- test-suite/typeclasses/NewSetoid.v | 10 ++++++---- theories/Arith/Arith.v | 10 ++++++---- theories/Arith/Arith_base.v | 10 ++++++---- theories/Arith/Between.v | 10 ++++++---- theories/Arith/Bool_nat.v | 10 ++++++---- theories/Arith/Compare.v | 10 ++++++---- theories/Arith/Compare_dec.v | 10 ++++++---- theories/Arith/Div2.v | 10 ++++++---- theories/Arith/EqNat.v | 10 ++++++---- theories/Arith/Euclid.v | 10 ++++++---- theories/Arith/Even.v | 10 ++++++---- theories/Arith/Factorial.v | 10 ++++++---- theories/Arith/Gt.v | 10 ++++++---- theories/Arith/Le.v | 10 ++++++---- theories/Arith/Lt.v | 10 ++++++---- theories/Arith/Max.v | 10 ++++++---- theories/Arith/Min.v | 10 ++++++---- theories/Arith/Minus.v | 10 ++++++---- theories/Arith/Mult.v | 10 ++++++---- theories/Arith/PeanoNat.v | 10 ++++++---- theories/Arith/Peano_dec.v | 10 ++++++---- theories/Arith/Plus.v | 12 +++++++----- theories/Arith/Wf_nat.v | 10 ++++++---- theories/Bool/Bool.v | 10 ++++++---- theories/Bool/BoolEq.v | 10 ++++++---- theories/Bool/Bvector.v | 10 ++++++---- theories/Bool/DecBool.v | 10 ++++++---- theories/Bool/IfProp.v | 10 ++++++---- theories/Bool/Sumbool.v | 10 ++++++---- theories/Bool/Zerob.v | 10 ++++++---- theories/Classes/CEquivalence.v | 10 ++++++---- theories/Classes/CMorphisms.v | 10 ++++++---- theories/Classes/CRelationClasses.v | 10 ++++++---- theories/Classes/DecidableClass.v | 10 ++++++---- theories/Classes/EquivDec.v | 10 ++++++---- theories/Classes/Equivalence.v | 10 ++++++---- theories/Classes/Init.v | 10 ++++++---- theories/Classes/Morphisms.v | 10 ++++++---- theories/Classes/Morphisms_Prop.v | 10 ++++++---- theories/Classes/Morphisms_Relations.v | 10 ++++++---- theories/Classes/RelationClasses.v | 10 ++++++---- theories/Classes/RelationPairs.v | 16 +++++++++------- theories/Classes/SetoidClass.v | 10 ++++++---- theories/Classes/SetoidDec.v | 10 ++++++---- theories/Classes/SetoidTactics.v | 10 ++++++---- theories/Compat/AdmitAxiom.v | 10 ++++++---- theories/Compat/Coq85.v | 10 ++++++---- theories/Compat/Coq86.v | 10 ++++++---- theories/Compat/Coq87.v | 10 ++++++---- theories/FSets/FMapAVL.v | 16 +++++++++------- theories/FSets/FMapFacts.v | 16 +++++++++------- theories/FSets/FMapFullAVL.v | 16 +++++++++------- theories/FSets/FMapInterface.v | 16 +++++++++------- theories/FSets/FMapList.v | 16 +++++++++------- theories/FSets/FMapPositive.v | 16 +++++++++------- theories/FSets/FMapWeakList.v | 16 +++++++++------- theories/FSets/FMaps.v | 16 +++++++++------- theories/FSets/FSetAVL.v | 16 +++++++++------- theories/FSets/FSetBridge.v | 16 +++++++++------- theories/FSets/FSetCompat.v | 16 +++++++++------- theories/FSets/FSetDecide.v | 16 +++++++++------- theories/FSets/FSetEqProperties.v | 16 +++++++++------- theories/FSets/FSetFacts.v | 16 +++++++++------- theories/FSets/FSetInterface.v | 16 +++++++++------- theories/FSets/FSetList.v | 16 +++++++++------- theories/FSets/FSetPositive.v | 16 +++++++++------- theories/FSets/FSetProperties.v | 16 +++++++++------- theories/FSets/FSetToFiniteSet.v | 16 +++++++++------- theories/FSets/FSetWeakList.v | 16 +++++++++------- theories/FSets/FSets.v | 16 +++++++++------- theories/Init/Datatypes.v | 10 ++++++---- theories/Init/Decimal.v | 10 ++++++---- theories/Init/Logic.v | 10 ++++++---- theories/Init/Logic_Type.v | 10 ++++++---- theories/Init/Nat.v | 10 ++++++---- theories/Init/Notations.v | 10 ++++++---- theories/Init/Peano.v | 10 ++++++---- theories/Init/Prelude.v | 10 ++++++---- theories/Init/Specif.v | 10 ++++++---- theories/Init/Tactics.v | 10 ++++++---- theories/Init/Wf.v | 10 ++++++---- theories/Lists/List.v | 10 ++++++---- theories/Lists/ListDec.v | 10 ++++++---- theories/Lists/ListSet.v | 10 ++++++---- theories/Lists/ListTactics.v | 10 ++++++---- theories/Lists/SetoidList.v | 16 +++++++++------- theories/Lists/SetoidPermutation.v | 16 +++++++++------- theories/Lists/StreamMemo.v | 10 ++++++---- theories/Lists/Streams.v | 10 ++++++---- theories/Logic/Berardi.v | 10 ++++++---- theories/Logic/ChoiceFacts.v | 12 +++++++----- theories/Logic/Classical.v | 10 ++++++---- theories/Logic/ClassicalChoice.v | 10 ++++++---- theories/Logic/ClassicalDescription.v | 10 ++++++---- theories/Logic/ClassicalEpsilon.v | 12 +++++++----- theories/Logic/ClassicalFacts.v | 10 ++++++---- theories/Logic/ClassicalUniqueChoice.v | 10 ++++++---- theories/Logic/Classical_Pred_Type.v | 10 ++++++---- theories/Logic/Classical_Prop.v | 10 ++++++---- theories/Logic/ConstructiveEpsilon.v | 10 ++++++---- theories/Logic/Decidable.v | 10 ++++++---- theories/Logic/Description.v | 10 ++++++---- theories/Logic/Diaconescu.v | 10 ++++++---- theories/Logic/Epsilon.v | 10 ++++++---- theories/Logic/Eqdep.v | 10 ++++++---- theories/Logic/EqdepFacts.v | 10 ++++++---- theories/Logic/Eqdep_dec.v | 10 ++++++---- theories/Logic/ExtensionalFunctionRepresentative.v | 10 ++++++---- theories/Logic/ExtensionalityFacts.v | 10 ++++++---- theories/Logic/FinFun.v | 10 ++++++---- theories/Logic/FunctionalExtensionality.v | 10 ++++++---- theories/Logic/Hurkens.v | 10 ++++++---- theories/Logic/IndefiniteDescription.v | 10 ++++++---- theories/Logic/JMeq.v | 10 ++++++---- theories/Logic/ProofIrrelevance.v | 10 ++++++---- theories/Logic/ProofIrrelevanceFacts.v | 10 ++++++---- theories/Logic/PropExtensionality.v | 10 ++++++---- theories/Logic/PropExtensionalityFacts.v | 10 ++++++---- theories/Logic/PropFacts.v | 10 ++++++---- theories/Logic/RelationalChoice.v | 10 ++++++---- theories/Logic/SetIsType.v | 10 ++++++---- theories/Logic/SetoidChoice.v | 10 ++++++---- theories/Logic/WKL.v | 10 ++++++---- theories/Logic/WeakFan.v | 10 ++++++---- theories/MSets/MSetAVL.v | 16 +++++++++------- theories/MSets/MSetDecide.v | 16 +++++++++------- theories/MSets/MSetEqProperties.v | 16 +++++++++------- theories/MSets/MSetFacts.v | 16 +++++++++------- theories/MSets/MSetGenTree.v | 16 +++++++++------- theories/MSets/MSetInterface.v | 16 +++++++++------- theories/MSets/MSetList.v | 16 +++++++++------- theories/MSets/MSetPositive.v | 16 +++++++++------- theories/MSets/MSetProperties.v | 16 +++++++++------- theories/MSets/MSetRBT.v | 16 +++++++++------- theories/MSets/MSetToFiniteSet.v | 16 +++++++++------- theories/MSets/MSetWeakList.v | 16 +++++++++------- theories/MSets/MSets.v | 16 +++++++++------- theories/NArith/BinNat.v | 10 ++++++---- theories/NArith/BinNatDef.v | 10 ++++++---- theories/NArith/NArith.v | 10 ++++++---- theories/NArith/Ndec.v | 10 ++++++---- theories/NArith/Ndigits.v | 10 ++++++---- theories/NArith/Ndist.v | 10 ++++++---- theories/NArith/Ndiv_def.v | 10 ++++++---- theories/NArith/Ngcd_def.v | 10 ++++++---- theories/NArith/Nnat.v | 10 ++++++---- theories/NArith/Nsqrt_def.v | 10 ++++++---- theories/Numbers/BinNums.v | 10 ++++++---- theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 10 ++++++---- theories/Numbers/Cyclic/Abstract/DoubleType.v | 10 ++++++---- theories/Numbers/Cyclic/Abstract/NZCyclic.v | 10 ++++++---- theories/Numbers/Cyclic/Int31/Cyclic31.v | 10 ++++++---- theories/Numbers/Cyclic/Int31/Int31.v | 10 ++++++---- theories/Numbers/Cyclic/Int31/Ring31.v | 10 ++++++---- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 10 ++++++---- theories/Numbers/DecimalFacts.v | 10 ++++++---- theories/Numbers/DecimalN.v | 10 ++++++---- theories/Numbers/DecimalNat.v | 10 ++++++---- theories/Numbers/DecimalPos.v | 10 ++++++---- theories/Numbers/DecimalString.v | 10 ++++++---- theories/Numbers/DecimalZ.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZAdd.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZAddOrder.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZAxioms.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZBase.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZBits.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZDivEucl.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZDivFloor.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZGcd.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZLcm.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZLt.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZMaxMin.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZMul.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZMulOrder.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZParity.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZPow.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZProperties.v | 10 ++++++---- theories/Numbers/Integer/Abstract/ZSgnAbs.v | 10 ++++++---- theories/Numbers/Integer/Binary/ZBinary.v | 10 ++++++---- theories/Numbers/Integer/NatPairs/ZNatPairs.v | 10 ++++++---- theories/Numbers/NaryFunctions.v | 10 ++++++---- theories/Numbers/NatInt/NZAdd.v | 10 ++++++---- theories/Numbers/NatInt/NZAddOrder.v | 10 ++++++---- theories/Numbers/NatInt/NZAxioms.v | 10 ++++++---- theories/Numbers/NatInt/NZBase.v | 10 ++++++---- theories/Numbers/NatInt/NZBits.v | 10 ++++++---- theories/Numbers/NatInt/NZDiv.v | 10 ++++++---- theories/Numbers/NatInt/NZDomain.v | 10 ++++++---- theories/Numbers/NatInt/NZGcd.v | 10 ++++++---- theories/Numbers/NatInt/NZLog.v | 10 ++++++---- theories/Numbers/NatInt/NZMul.v | 10 ++++++---- theories/Numbers/NatInt/NZMulOrder.v | 10 ++++++---- theories/Numbers/NatInt/NZOrder.v | 10 ++++++---- theories/Numbers/NatInt/NZParity.v | 10 ++++++---- theories/Numbers/NatInt/NZPow.v | 10 ++++++---- theories/Numbers/NatInt/NZProperties.v | 10 ++++++---- theories/Numbers/NatInt/NZSqrt.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NAdd.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NAddOrder.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NAxioms.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NBase.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NBits.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NDefOps.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NDiv.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NGcd.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NIso.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NLcm.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NLog.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NMaxMin.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NMulOrder.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NOrder.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NParity.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NPow.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NProperties.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NSqrt.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NStrongRec.v | 10 ++++++---- theories/Numbers/Natural/Abstract/NSub.v | 10 ++++++---- theories/Numbers/Natural/Binary/NBinary.v | 10 ++++++---- theories/Numbers/Natural/Peano/NPeano.v | 10 ++++++---- theories/Numbers/NumPrelude.v | 10 ++++++---- theories/PArith/BinPos.v | 10 ++++++---- theories/PArith/BinPosDef.v | 10 ++++++---- theories/PArith/PArith.v | 10 ++++++---- theories/PArith/POrderedType.v | 10 ++++++---- theories/PArith/Pnat.v | 10 ++++++---- theories/Program/Basics.v | 10 ++++++---- theories/Program/Combinators.v | 10 ++++++---- theories/Program/Equality.v | 10 ++++++---- theories/Program/Program.v | 10 ++++++---- theories/Program/Subset.v | 10 ++++++---- theories/Program/Syntax.v | 10 ++++++---- theories/Program/Tactics.v | 10 ++++++---- theories/Program/Utils.v | 10 ++++++---- theories/Program/Wf.v | 10 ++++++---- theories/QArith/QArith.v | 10 ++++++---- theories/QArith/QArith_base.v | 10 ++++++---- theories/QArith/QOrderedType.v | 10 ++++++---- theories/QArith/Qabs.v | 10 ++++++---- theories/QArith/Qcabs.v | 10 ++++++---- theories/QArith/Qcanon.v | 10 ++++++---- theories/QArith/Qfield.v | 10 ++++++---- theories/QArith/Qminmax.v | 10 ++++++---- theories/QArith/Qpower.v | 10 ++++++---- theories/QArith/Qreals.v | 10 ++++++---- theories/QArith/Qreduction.v | 10 ++++++---- theories/QArith/Qring.v | 10 ++++++---- theories/QArith/Qround.v | 10 ++++++---- theories/Reals/Alembert.v | 10 ++++++---- theories/Reals/AltSeries.v | 10 ++++++---- theories/Reals/ArithProp.v | 10 ++++++---- theories/Reals/Binomial.v | 10 ++++++---- theories/Reals/Cauchy_prod.v | 10 ++++++---- theories/Reals/Cos_plus.v | 10 ++++++---- theories/Reals/Cos_rel.v | 10 ++++++---- theories/Reals/DiscrR.v | 10 ++++++---- theories/Reals/Exp_prop.v | 10 ++++++---- theories/Reals/Integration.v | 10 ++++++---- theories/Reals/MVT.v | 10 ++++++---- theories/Reals/Machin.v | 10 ++++++---- theories/Reals/NewtonInt.v | 10 ++++++---- theories/Reals/PSeries_reg.v | 10 ++++++---- theories/Reals/PartSum.v | 10 ++++++---- theories/Reals/RIneq.v | 12 +++++++----- theories/Reals/RList.v | 10 ++++++---- theories/Reals/ROrderedType.v | 10 ++++++---- theories/Reals/R_Ifp.v | 10 ++++++---- theories/Reals/R_sqr.v | 10 ++++++---- theories/Reals/R_sqrt.v | 10 ++++++---- theories/Reals/Ranalysis.v | 10 ++++++---- theories/Reals/Ranalysis1.v | 10 ++++++---- theories/Reals/Ranalysis2.v | 10 ++++++---- theories/Reals/Ranalysis3.v | 10 ++++++---- theories/Reals/Ranalysis4.v | 10 ++++++---- theories/Reals/Ranalysis5.v | 10 ++++++---- theories/Reals/Ranalysis_reg.v | 10 ++++++---- theories/Reals/Ratan.v | 10 ++++++---- theories/Reals/Raxioms.v | 10 ++++++---- theories/Reals/Rbase.v | 10 ++++++---- theories/Reals/Rbasic_fun.v | 10 ++++++---- theories/Reals/Rcomplete.v | 10 ++++++---- theories/Reals/Rdefinitions.v | 10 ++++++---- theories/Reals/Rderiv.v | 10 ++++++---- theories/Reals/Reals.v | 10 ++++++---- theories/Reals/Rfunctions.v | 10 ++++++---- theories/Reals/Rgeom.v | 10 ++++++---- theories/Reals/RiemannInt.v | 10 ++++++---- theories/Reals/RiemannInt_SF.v | 10 ++++++---- theories/Reals/Rlimit.v | 10 ++++++---- theories/Reals/Rlogic.v | 10 ++++++---- theories/Reals/Rminmax.v | 10 ++++++---- theories/Reals/Rpow_def.v | 10 ++++++---- theories/Reals/Rpower.v | 10 ++++++---- theories/Reals/Rprod.v | 10 ++++++---- theories/Reals/Rseries.v | 10 ++++++---- theories/Reals/Rsigma.v | 10 ++++++---- theories/Reals/Rsqrt_def.v | 10 ++++++---- theories/Reals/Rtopology.v | 10 ++++++---- theories/Reals/Rtrigo.v | 10 ++++++---- theories/Reals/Rtrigo1.v | 10 ++++++---- theories/Reals/Rtrigo_alt.v | 10 ++++++---- theories/Reals/Rtrigo_calc.v | 10 ++++++---- theories/Reals/Rtrigo_def.v | 10 ++++++---- theories/Reals/Rtrigo_fun.v | 10 ++++++---- theories/Reals/Rtrigo_reg.v | 10 ++++++---- theories/Reals/SeqProp.v | 10 ++++++---- theories/Reals/SeqSeries.v | 10 ++++++---- theories/Reals/SplitAbsolu.v | 10 ++++++---- theories/Reals/SplitRmult.v | 10 ++++++---- theories/Reals/Sqrt_reg.v | 10 ++++++---- theories/Relations/Operators_Properties.v | 10 ++++++---- theories/Relations/Relation_Definitions.v | 10 ++++++---- theories/Relations/Relation_Operators.v | 10 ++++++---- theories/Relations/Relations.v | 10 ++++++---- theories/Setoids/Setoid.v | 10 ++++++---- theories/Sets/Classical_sets.v | 10 ++++++---- theories/Sets/Constructive_sets.v | 10 ++++++---- theories/Sets/Cpo.v | 10 ++++++---- theories/Sets/Ensembles.v | 10 ++++++---- theories/Sets/Finite_sets.v | 10 ++++++---- theories/Sets/Finite_sets_facts.v | 10 ++++++---- theories/Sets/Image.v | 10 ++++++---- theories/Sets/Infinite_sets.v | 10 ++++++---- theories/Sets/Integers.v | 10 ++++++---- theories/Sets/Multiset.v | 10 ++++++---- theories/Sets/Partial_Order.v | 10 ++++++---- theories/Sets/Permut.v | 10 ++++++---- theories/Sets/Powerset.v | 10 ++++++---- theories/Sets/Powerset_Classical_facts.v | 10 ++++++---- theories/Sets/Powerset_facts.v | 10 ++++++---- theories/Sets/Relations_1.v | 10 ++++++---- theories/Sets/Relations_1_facts.v | 10 ++++++---- theories/Sets/Relations_2.v | 10 ++++++---- theories/Sets/Relations_2_facts.v | 10 ++++++---- theories/Sets/Relations_3.v | 10 ++++++---- theories/Sets/Relations_3_facts.v | 10 ++++++---- theories/Sets/Uniset.v | 10 ++++++---- theories/Sorting/Heap.v | 10 ++++++---- theories/Sorting/Mergesort.v | 10 ++++++---- theories/Sorting/PermutEq.v | 10 ++++++---- theories/Sorting/PermutSetoid.v | 10 ++++++---- theories/Sorting/Permutation.v | 10 ++++++---- theories/Sorting/Sorted.v | 10 ++++++---- theories/Sorting/Sorting.v | 10 ++++++---- theories/Strings/Ascii.v | 12 +++++++----- theories/Strings/String.v | 10 ++++++---- theories/Structures/DecidableType.v | 16 +++++++++------- theories/Structures/DecidableTypeEx.v | 16 +++++++++------- theories/Structures/Equalities.v | 16 +++++++++------- theories/Structures/EqualitiesFacts.v | 16 +++++++++------- theories/Structures/GenericMinMax.v | 16 +++++++++------- theories/Structures/OrderedType.v | 16 +++++++++------- theories/Structures/OrderedTypeAlt.v | 16 +++++++++------- theories/Structures/OrderedTypeEx.v | 16 +++++++++------- theories/Structures/Orders.v | 16 +++++++++------- theories/Structures/OrdersAlt.v | 16 +++++++++------- theories/Structures/OrdersEx.v | 16 +++++++++------- theories/Structures/OrdersFacts.v | 16 +++++++++------- theories/Structures/OrdersLists.v | 16 +++++++++------- theories/Structures/OrdersTac.v | 16 +++++++++------- theories/Unicode/Utf8.v | 10 ++++++---- theories/Unicode/Utf8_core.v | 10 ++++++---- theories/Vectors/Fin.v | 10 ++++++---- theories/Vectors/Vector.v | 10 ++++++---- theories/Vectors/VectorDef.v | 10 ++++++---- theories/Vectors/VectorEq.v | 10 ++++++---- theories/Vectors/VectorSpec.v | 10 ++++++---- theories/Wellfounded/Disjoint_Union.v | 10 ++++++---- theories/Wellfounded/Inclusion.v | 10 ++++++---- theories/Wellfounded/Inverse_Image.v | 10 ++++++---- theories/Wellfounded/Lexicographic_Exponentiation.v | 10 ++++++---- theories/Wellfounded/Lexicographic_Product.v | 10 ++++++---- theories/Wellfounded/Transitive_Closure.v | 10 ++++++---- theories/Wellfounded/Union.v | 10 ++++++---- theories/Wellfounded/Well_Ordering.v | 10 ++++++---- theories/Wellfounded/Wellfounded.v | 10 ++++++---- theories/ZArith/BinInt.v | 10 ++++++---- theories/ZArith/BinIntDef.v | 10 ++++++---- theories/ZArith/Int.v | 16 +++++++++------- theories/ZArith/Wf_Z.v | 10 ++++++---- theories/ZArith/ZArith.v | 10 ++++++---- theories/ZArith/ZArith_base.v | 10 ++++++---- theories/ZArith/ZArith_dec.v | 10 ++++++---- theories/ZArith/Zabs.v | 10 ++++++---- theories/ZArith/Zbool.v | 10 ++++++---- theories/ZArith/Zcompare.v | 10 ++++++---- theories/ZArith/Zcomplements.v | 10 ++++++---- theories/ZArith/Zdigits.v | 10 ++++++---- theories/ZArith/Zdiv.v | 10 ++++++---- theories/ZArith/Zeuclid.v | 10 ++++++---- theories/ZArith/Zeven.v | 10 ++++++---- theories/ZArith/Zgcd_alt.v | 10 ++++++---- theories/ZArith/Zhints.v | 10 ++++++---- theories/ZArith/Zlogarithm.v | 10 ++++++---- theories/ZArith/Zmax.v | 10 ++++++---- theories/ZArith/Zmin.v | 10 ++++++---- theories/ZArith/Zminmax.v | 10 ++++++---- theories/ZArith/Zmisc.v | 10 ++++++---- theories/ZArith/Znat.v | 10 ++++++---- theories/ZArith/Znumtheory.v | 10 ++++++---- theories/ZArith/Zorder.v | 10 ++++++---- theories/ZArith/Zpow_alt.v | 10 ++++++---- theories/ZArith/Zpow_def.v | 10 ++++++---- theories/ZArith/Zpow_facts.v | 10 ++++++---- theories/ZArith/Zpower.v | 10 ++++++---- theories/ZArith/Zquot.v | 10 ++++++---- theories/ZArith/Zsqrt_compat.v | 10 ++++++---- theories/ZArith/Zwf.v | 10 ++++++---- theories/ZArith/auxiliary.v | 10 ++++++---- tools/coq_makefile.ml | 10 ++++++---- tools/coq_tex.ml | 10 ++++++---- tools/coqc.ml | 10 ++++++---- tools/coqdep.ml | 10 ++++++---- tools/coqdep_boot.ml | 10 ++++++---- tools/coqdep_common.ml | 10 ++++++---- tools/coqdep_common.mli | 10 ++++++---- tools/coqdep_lexer.mli | 10 ++++++---- tools/coqdep_lexer.mll | 10 ++++++---- tools/coqdoc/alpha.ml | 10 ++++++---- tools/coqdoc/alpha.mli | 10 ++++++---- tools/coqdoc/cdglobals.ml | 10 ++++++---- tools/coqdoc/cpretty.mli | 10 ++++++---- tools/coqdoc/cpretty.mll | 10 ++++++---- tools/coqdoc/index.ml | 10 ++++++---- tools/coqdoc/index.mli | 10 ++++++---- tools/coqdoc/main.ml | 10 ++++++---- tools/coqdoc/output.ml | 10 ++++++---- tools/coqdoc/output.mli | 10 ++++++---- tools/coqdoc/tokens.ml | 10 ++++++---- tools/coqdoc/tokens.mli | 10 ++++++---- tools/coqwc.mll | 10 ++++++---- tools/coqworkmgr.ml | 10 ++++++---- tools/fake_ide.ml | 10 ++++++---- tools/gallina.ml | 10 ++++++---- tools/gallina_lexer.mll | 10 ++++++---- tools/ocamllibdep.mll | 10 ++++++---- toplevel/coqargs.ml | 10 ++++++---- toplevel/coqargs.mli | 10 ++++++---- toplevel/coqinit.ml | 10 ++++++---- toplevel/coqinit.mli | 10 ++++++---- toplevel/coqloop.ml | 10 ++++++---- toplevel/coqloop.mli | 10 ++++++---- toplevel/coqtop.ml | 10 ++++++---- toplevel/coqtop.mli | 10 ++++++---- toplevel/usage.ml | 10 ++++++---- toplevel/usage.mli | 10 ++++++---- toplevel/vernac.ml | 10 ++++++---- toplevel/vernac.mli | 10 ++++++---- vernac/assumptions.ml | 10 ++++++---- vernac/assumptions.mli | 10 ++++++---- vernac/auto_ind_decl.ml | 10 ++++++---- vernac/auto_ind_decl.mli | 10 ++++++---- vernac/class.ml | 10 ++++++---- vernac/class.mli | 10 ++++++---- vernac/classes.ml | 10 ++++++---- vernac/classes.mli | 10 ++++++---- vernac/comAssumption.ml | 10 ++++++---- vernac/comAssumption.mli | 10 ++++++---- vernac/comDefinition.ml | 10 ++++++---- vernac/comDefinition.mli | 10 ++++++---- vernac/comFixpoint.mli | 10 ++++++---- vernac/comInductive.ml | 10 ++++++---- vernac/comInductive.mli | 10 ++++++---- vernac/declareDef.ml | 10 ++++++---- vernac/declareDef.mli | 10 ++++++---- vernac/explainErr.ml | 10 ++++++---- vernac/explainErr.mli | 10 ++++++---- vernac/himsg.ml | 10 ++++++---- vernac/himsg.mli | 10 ++++++---- vernac/indschemes.ml | 10 ++++++---- vernac/indschemes.mli | 10 ++++++---- vernac/lemmas.ml | 10 ++++++---- vernac/lemmas.mli | 10 ++++++---- vernac/locality.ml | 10 ++++++---- vernac/locality.mli | 10 ++++++---- vernac/metasyntax.ml | 10 ++++++---- vernac/metasyntax.mli | 10 ++++++---- vernac/mltop.ml | 10 ++++++---- vernac/mltop.mli | 10 ++++++---- vernac/obligations.mli | 10 ++++++---- vernac/proof_using.ml | 10 ++++++---- vernac/proof_using.mli | 10 ++++++---- vernac/record.ml | 10 ++++++---- vernac/record.mli | 10 ++++++---- vernac/search.ml | 10 ++++++---- vernac/search.mli | 10 ++++++---- vernac/topfmt.ml | 10 ++++++---- vernac/topfmt.mli | 10 ++++++---- vernac/vernacentries.ml | 10 ++++++---- vernac/vernacentries.mli | 10 ++++++---- vernac/vernacinterp.ml | 10 ++++++---- vernac/vernacinterp.mli | 10 ++++++---- vernac/vernacprop.ml | 10 ++++++---- vernac/vernacprop.mli | 10 ++++++---- vernac/vernacstate.ml | 10 ++++++---- vernac/vernacstate.mli | 10 ++++++---- 1356 files changed, 8399 insertions(+), 5680 deletions(-) diff --git a/Makefile b/Makefile index 0c9bccc83..03b6e576f 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,12 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# unit diff --git a/checker/cic.mli b/checker/cic.mli index 1f4322dff..42629ced2 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Names.ModPath.t -> Cic.module_body -> unit diff --git a/checker/modops.ml b/checker/modops.ml index f0abc39ea..c7ad0977a 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Values.value -> 'a -> unit diff --git a/checker/values.ml b/checker/values.ml index 283adca03..160653d9b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* int type 'a eq = 'a -> 'a -> bool diff --git a/clib/cList.mli b/clib/cList.mli index b3ee28548..db37050aa 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* int type 'a eq = 'a -> 'a -> bool diff --git a/clib/cMap.ml b/clib/cMap.ml index b4c4aedd0..373e3f8fd 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string list Util.String.Map.t -> unit diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index eb575b95f..55d8d9698 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* GText.tag -> unit) -> string -> unit diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index fcc242e07..1fdd7317b 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit diff --git a/ide/document.ml b/ide/document.ml index 62457fe56..0d3b36a7f 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* GMisc.image diff --git a/ide/interface.mli b/ide/interface.mli index a5d98946f..debbc8301 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* () diff --git a/ide/minilib.mli b/ide/minilib.mli index 4f5fbe7db..6cc36f5f2 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string diff --git a/ide/preferences.ml b/ide/preferences.ml index 7c251f79c..11aaf6e8c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 6a9e23879..6e36ae1c8 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Coq.coqtop -> CoqOps.coqops -> diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index f87730461..6a9317bc2 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* GText.view -> diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 65df2b849..74f687ef7 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit diff --git a/interp/genintern.ml b/interp/genintern.ml index 2f2edab30..161201c44 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* diff --git a/lib/future.mli b/lib/future.mli index 853f81cea..d9e8c87b2 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli index c262e50e5..ae0605cfb 100644 --- a/lib/remoteCounter.mli +++ b/lib/remoteCounter.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit Proofview.tactic diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 609ca62a0..5db587b9c 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* : non commutative polynomials on a commutative ring A *) diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 25afeaa7f..795850781 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Entries.mutual_inductive_entry -> diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 86bc47132..1664e68f2 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* diff --git a/printing/prettyp.mli b/printing/prettyp.mli index c1d8f1d37..213f0aeeb 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 04062fbbd..d6b386f10 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Cdglobals.coq_module -> unit diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 186f6cf6c..1be440a75 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* on 9 & 10 Mar 2004: diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d043c4a58..d25227002 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*