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

    • This research was partly supported by IST diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html index 1641a1ed3..328bd68da 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -38,7 +38,7 @@

  • V8.2 © INRIA 2008-2011
  • V8.3 © INRIA 2010-2011
  • V8.4 © INRIA 2012-2014
    • -
  • V8.5 © INRIA 2015
    • +
  • V8.5 © INRIA 2015-2016

    • This research was partly supported by IST diff --git a/doc/common/title.tex b/doc/common/title.tex index 4716c3156..0e072b6b6 100644 --- a/doc/common/title.tex +++ b/doc/common/title.tex @@ -45,7 +45,7 @@ V\coqversion, \today %END LATEX \copyright INRIA 1999-2004 ({\Coq} versions 7.x) -\copyright INRIA 2004-2015 ({\Coq} versions 8.x) +\copyright INRIA 2004-2016 ({\Coq} versions 8.x) #3 \end{flushleft} diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index fe0959ddb..8def9537c 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* CFBundleGetInfoString Coq_vVERSION NSHumanReadableCopyright - Copyright 1999-2015, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS + Copyright 1999-2016, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS CFBundleHelpBookFolder share/doc/coq/html/ CFAppleHelpAnchor diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 367153568..ac9cc57bc 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*