From 763cf4f37e10d9a0e8a2a0e9286c02708a60bf08 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 16 Jul 2004 20:01:26 +0000 Subject: Nouvelle en-tĂȘte MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7 --- config/coq_config.mli | 14 ++++---- contrib/cc/CCSolve.v | 14 ++++---- contrib/cc/ccalgo.ml | 14 ++++---- contrib/cc/ccalgo.mli | 14 ++++---- contrib/cc/ccproof.ml | 14 ++++---- contrib/cc/ccproof.mli | 14 ++++---- contrib/cc/cctac.ml4 | 14 ++++---- contrib/correctness/ArrayPermut.v | 14 ++++---- contrib/correctness/Arrays.v | 14 ++++---- contrib/correctness/Arrays_stuff.v | 14 ++++---- contrib/correctness/Correctness.v | 14 ++++---- contrib/correctness/Exchange.v | 14 ++++---- contrib/correctness/ProgBool.v | 14 ++++---- contrib/correctness/ProgInt.v | 14 ++++---- contrib/correctness/ProgramsExtraction.v | 14 ++++---- contrib/correctness/Programs_stuff.v | 14 ++++---- contrib/correctness/Sorted.v | 14 ++++---- contrib/correctness/Tuples.v | 14 ++++---- contrib/correctness/past.mli | 14 ++++---- contrib/correctness/pcic.ml | 14 ++++---- contrib/correctness/pcic.mli | 14 ++++---- contrib/correctness/pcicenv.ml | 14 ++++---- contrib/correctness/pcicenv.mli | 14 ++++---- contrib/correctness/pdb.ml | 14 ++++---- contrib/correctness/pdb.mli | 14 ++++---- contrib/correctness/peffect.ml | 14 ++++---- contrib/correctness/peffect.mli | 14 ++++---- contrib/correctness/penv.ml | 14 ++++---- contrib/correctness/penv.mli | 14 ++++---- contrib/correctness/perror.ml | 14 ++++---- contrib/correctness/perror.mli | 14 ++++---- contrib/correctness/pextract.ml | 14 ++++---- contrib/correctness/pextract.mli | 14 ++++---- contrib/correctness/pmisc.ml | 14 ++++---- contrib/correctness/pmisc.mli | 14 ++++---- contrib/correctness/pmlize.ml | 14 ++++---- contrib/correctness/pmlize.mli | 14 ++++---- contrib/correctness/pmonad.ml | 14 ++++---- contrib/correctness/pmonad.mli | 14 ++++---- contrib/correctness/pred.ml | 14 ++++---- contrib/correctness/pred.mli | 14 ++++---- contrib/correctness/prename.ml | 14 ++++---- contrib/correctness/prename.mli | 14 ++++---- contrib/correctness/psyntax.ml4 | 14 ++++---- contrib/correctness/psyntax.mli | 14 ++++---- contrib/correctness/ptactic.ml | 14 ++++---- contrib/correctness/ptactic.mli | 14 ++++---- contrib/correctness/ptype.mli | 14 ++++---- contrib/correctness/ptyping.ml | 14 ++++---- contrib/correctness/ptyping.mli | 14 ++++---- contrib/correctness/putil.ml | 14 ++++---- contrib/correctness/putil.mli | 14 ++++---- contrib/correctness/pwp.ml | 14 ++++---- contrib/correctness/pwp.mli | 14 ++++---- contrib/extraction/common.ml | 14 ++++---- contrib/extraction/common.mli | 14 ++++---- contrib/extraction/extract_env.ml | 14 ++++---- contrib/extraction/extract_env.mli | 14 ++++---- contrib/extraction/extraction.ml | 14 ++++---- contrib/extraction/extraction.mli | 14 ++++---- contrib/extraction/g_extraction.ml4 | 14 ++++---- contrib/extraction/haskell.ml | 14 ++++---- contrib/extraction/haskell.mli | 14 ++++---- contrib/extraction/miniml.mli | 14 ++++---- contrib/extraction/mlutil.ml | 14 ++++---- contrib/extraction/mlutil.mli | 14 ++++---- contrib/extraction/modutil.ml | 14 ++++---- contrib/extraction/modutil.mli | 14 ++++---- contrib/extraction/ocaml.ml | 14 ++++---- contrib/extraction/ocaml.mli | 14 ++++---- contrib/extraction/scheme.ml | 14 ++++---- contrib/extraction/scheme.mli | 14 ++++---- contrib/extraction/table.ml | 14 ++++---- contrib/extraction/table.mli | 14 ++++---- contrib/extraction/test_extraction.v | 14 ++++---- contrib/field/Field.v | 14 ++++---- contrib/field/Field_Compl.v | 14 ++++---- contrib/field/Field_Tactic.v | 14 ++++---- contrib/field/Field_Theory.v | 14 ++++---- contrib/field/field.ml4 | 14 ++++---- contrib/first-order/formula.ml | 14 ++++---- contrib/first-order/formula.mli | 14 ++++---- contrib/first-order/g_ground.ml4 | 14 ++++---- contrib/first-order/ground.ml | 14 ++++---- contrib/first-order/ground.mli | 14 ++++---- contrib/first-order/instances.ml | 14 ++++---- contrib/first-order/instances.mli | 14 ++++---- contrib/first-order/rules.ml | 14 ++++---- contrib/first-order/rules.mli | 14 ++++---- contrib/first-order/sequent.ml | 14 ++++---- contrib/first-order/sequent.mli | 14 ++++---- contrib/first-order/unify.ml | 14 ++++---- contrib/first-order/unify.mli | 14 ++++---- contrib/fourier/Fourier.v | 14 ++++---- contrib/fourier/Fourier_util.v | 14 ++++---- contrib/fourier/fourier.ml | 14 ++++---- contrib/fourier/fourierR.ml | 14 ++++---- contrib/fourier/g_fourier.ml4 | 14 ++++---- contrib/interface/blast.ml | 2 +- contrib/interface/showproof.ml | 2 +- contrib/omega/Omega.v | 14 ++++---- contrib/omega/OmegaLemmas.v | 14 ++++---- contrib/omega/coq_omega.ml | 14 ++++---- contrib/omega/g_omega.ml4 | 14 ++++---- contrib/omega/omega.ml | 14 ++++---- contrib/ring/ArithRing.v | 14 ++++---- contrib/ring/NArithRing.v | 14 ++++---- contrib/ring/Quote.v | 14 ++++---- contrib/ring/Ring.v | 14 ++++---- contrib/ring/Ring_abstract.v | 14 ++++---- contrib/ring/Ring_normalize.v | 14 ++++---- contrib/ring/Ring_theory.v | 14 ++++---- contrib/ring/Setoid_ring.v | 14 ++++---- contrib/ring/Setoid_ring_normalize.v | 14 ++++---- contrib/ring/Setoid_ring_theory.v | 14 ++++---- contrib/ring/ZArithRing.v | 14 ++++---- contrib/ring/g_quote.ml4 | 14 ++++---- contrib/ring/g_ring.ml4 | 14 ++++---- contrib/ring/quote.ml | 14 ++++---- contrib/ring/ring.ml | 14 ++++---- contrib/romega/omega2.ml | 14 ++++---- contrib/xml/acic.ml | 26 +++++++-------- contrib/xml/acic2Xml.ml4 | 26 +++++++-------- contrib/xml/cic2acic.ml | 26 +++++++-------- contrib/xml/doubleTypeInference.ml | 26 +++++++-------- contrib/xml/doubleTypeInference.mli | 26 +++++++-------- contrib/xml/proof2aproof.ml | 26 +++++++-------- contrib/xml/proofTree2Xml.ml4 | 26 +++++++-------- contrib/xml/unshare.ml | 26 +++++++-------- contrib/xml/unshare.mli | 26 +++++++-------- contrib/xml/xml.ml4 | 26 +++++++-------- contrib/xml/xml.mli | 26 +++++++-------- contrib/xml/xmlcommand.ml | 26 +++++++-------- contrib/xml/xmlcommand.mli | 26 +++++++-------- contrib/xml/xmlentries.ml4 | 26 +++++++-------- contrib7/cc/CCSolve.v | 14 ++++---- contrib7/correctness/ArrayPermut.v | 14 ++++---- contrib7/correctness/Arrays.v | 14 ++++---- contrib7/correctness/Arrays_stuff.v | 14 ++++---- contrib7/correctness/Correctness.v | 14 ++++---- contrib7/correctness/Exchange.v | 14 ++++---- contrib7/correctness/ProgBool.v | 14 ++++---- contrib7/correctness/ProgInt.v | 14 ++++---- contrib7/correctness/ProgramsExtraction.v | 14 ++++---- contrib7/correctness/Programs_stuff.v | 14 ++++---- contrib7/correctness/Sorted.v | 14 ++++---- contrib7/correctness/Tuples.v | 14 ++++---- contrib7/extraction/test_extraction.v | 14 ++++---- contrib7/field/Field.v | 14 ++++---- contrib7/field/Field_Compl.v | 14 ++++---- contrib7/field/Field_Tactic.v | 14 ++++---- contrib7/field/Field_Theory.v | 14 ++++---- contrib7/fourier/Fourier.v | 14 ++++---- contrib7/fourier/Fourier_util.v | 14 ++++---- contrib7/omega/Omega.v | 14 ++++---- contrib7/omega/OmegaLemmas.v | 14 ++++---- contrib7/ring/ArithRing.v | 14 ++++---- contrib7/ring/NArithRing.v | 14 ++++---- contrib7/ring/Quote.v | 14 ++++---- contrib7/ring/Ring.v | 14 ++++---- contrib7/ring/Ring_abstract.v | 14 ++++---- contrib7/ring/Ring_normalize.v | 14 ++++---- contrib7/ring/Ring_theory.v | 14 ++++---- contrib7/ring/Setoid_ring.v | 14 ++++---- contrib7/ring/Setoid_ring_normalize.v | 14 ++++---- contrib7/ring/Setoid_ring_theory.v | 14 ++++---- contrib7/ring/ZArithRing.v | 14 ++++---- dev/db_printers.ml | 14 ++++---- dev/top_printers.ml | 14 ++++---- ide/blaster_window.ml | 14 ++++---- ide/command_windows.ml | 14 ++++---- ide/command_windows.mli | 14 ++++---- ide/config_lexer.mll | 14 ++++---- ide/config_parser.mly | 10 +++--- ide/coq.ml | 14 ++++---- ide/coq.mli | 14 ++++---- ide/coq_commands.ml | 14 ++++---- ide/coq_tactics.ml | 14 ++++---- ide/coq_tactics.mli | 14 ++++---- ide/coqide.ml | 14 ++++---- ide/coqide.mli | 14 ++++---- ide/extract_index.mll | 14 ++++---- ide/find_phrase.mll | 14 ++++---- ide/highlight.mll | 14 ++++---- ide/ideutils.ml | 14 ++++---- ide/ideutils.mli | 14 ++++---- ide/preferences.ml | 14 ++++---- ide/preferences.mli | 14 ++++---- ide/undo.ml | 14 ++++---- ide/undo.mli | 14 ++++---- ide/utf8.v | 14 ++++---- ide/utf8_convert.mll | 14 ++++---- interp/constrextern.ml | 16 ++++----- interp/constrextern.mli | 14 ++++---- interp/constrintern.ml | 14 ++++---- interp/constrintern.mli | 14 ++++---- interp/coqlib.ml | 14 ++++---- interp/coqlib.mli | 14 ++++---- interp/genarg.ml | 14 ++++---- interp/genarg.mli | 14 ++++---- interp/modintern.ml | 14 ++++---- interp/modintern.mli | 14 ++++---- interp/ppextend.ml | 14 ++++---- interp/ppextend.mli | 14 ++++---- interp/reserve.ml | 14 ++++---- interp/reserve.mli | 14 ++++---- interp/symbols.ml | 14 ++++---- interp/symbols.mli | 14 ++++---- interp/syntax_def.ml | 14 ++++---- interp/syntax_def.mli | 14 ++++---- interp/topconstr.ml | 14 ++++---- interp/topconstr.mli | 14 ++++---- kernel/closure.ml | 18 +++++----- kernel/closure.mli | 22 ++++++------- kernel/conv_oracle.ml | 14 ++++---- kernel/conv_oracle.mli | 14 ++++---- kernel/cooking.ml | 14 ++++---- kernel/cooking.mli | 14 ++++---- kernel/declarations.ml | 14 ++++---- kernel/declarations.mli | 14 ++++---- kernel/entries.ml | 14 ++++---- kernel/entries.mli | 14 ++++---- kernel/environ.ml | 14 ++++---- kernel/environ.mli | 30 ++++++++--------- kernel/esubst.ml | 14 ++++---- kernel/esubst.mli | 14 ++++---- kernel/indtypes.ml | 32 +++++++++--------- kernel/indtypes.mli | 14 ++++---- kernel/inductive.ml | 38 +++++++++++----------- kernel/inductive.mli | 14 ++++---- kernel/mod_typing.ml | 14 ++++---- kernel/mod_typing.mli | 14 ++++---- kernel/modops.ml | 14 ++++---- kernel/modops.mli | 14 ++++---- kernel/names.ml | 14 ++++---- kernel/names.mli | 14 ++++---- kernel/reduction.ml | 14 ++++---- kernel/reduction.mli | 22 ++++++------- kernel/safe_typing.ml | 14 ++++---- kernel/safe_typing.mli | 14 ++++---- kernel/sign.ml | 14 ++++---- kernel/sign.mli | 14 ++++---- kernel/subtyping.ml | 14 ++++---- kernel/subtyping.mli | 14 ++++---- kernel/term.ml | 18 +++++----- kernel/term.mli | 14 ++++---- kernel/term_typing.ml | 14 ++++---- kernel/term_typing.mli | 14 ++++---- kernel/type_errors.ml | 14 ++++---- kernel/type_errors.mli | 14 ++++---- kernel/typeops.ml | 18 +++++----- kernel/typeops.mli | 14 ++++---- kernel/univ.ml | 14 ++++---- kernel/univ.mli | 14 ++++---- lib/bignat.ml | 14 ++++---- lib/bignat.mli | 14 ++++---- lib/bstack.ml | 14 ++++---- lib/bstack.mli | 14 ++++---- lib/dyn.ml | 14 ++++---- lib/dyn.mli | 14 ++++---- lib/edit.ml | 14 ++++---- lib/edit.mli | 14 ++++---- lib/explore.ml | 14 ++++---- lib/explore.mli | 14 ++++---- lib/gmap.ml | 14 ++++---- lib/gmap.mli | 14 ++++---- lib/gmapl.ml | 14 ++++---- lib/gmapl.mli | 14 ++++---- lib/gset.ml | 14 ++++---- lib/gset.mli | 14 ++++---- lib/hashcons.ml | 14 ++++---- lib/hashcons.mli | 14 ++++---- lib/heap.ml | 14 ++++---- lib/heap.mli | 14 ++++---- lib/options.ml | 14 ++++---- lib/options.mli | 14 ++++---- lib/pp.ml4 | 14 ++++---- lib/pp.mli | 14 ++++---- lib/pp_control.ml | 14 ++++---- lib/pp_control.mli | 14 ++++---- lib/predicate.ml | 4 +-- lib/profile.ml | 14 ++++---- lib/profile.mli | 14 ++++---- lib/rtree.ml | 14 ++++---- lib/rtree.mli | 14 ++++---- lib/stamps.ml | 14 ++++---- lib/stamps.mli | 14 ++++---- lib/system.ml | 14 ++++---- lib/system.mli | 14 ++++---- lib/tlm.ml | 14 ++++---- lib/tlm.mli | 14 ++++---- lib/util.ml | 14 ++++---- lib/util.mli | 14 ++++---- library/decl_kinds.ml | 14 ++++---- library/declare.ml | 14 ++++---- library/declare.mli | 14 ++++---- library/declaremods.ml | 16 ++++----- library/declaremods.mli | 14 ++++---- library/dischargedhypsmap.ml | 14 ++++---- library/dischargedhypsmap.mli | 14 ++++---- library/global.ml | 14 ++++---- library/global.mli | 14 ++++---- library/goptions.ml | 14 ++++---- library/goptions.mli | 14 ++++---- library/impargs.ml | 14 ++++---- library/impargs.mli | 14 ++++---- library/lib.ml | 14 ++++---- library/lib.mli | 14 ++++---- library/libnames.ml | 14 ++++---- library/libnames.mli | 14 ++++---- library/libobject.ml | 14 ++++---- library/libobject.mli | 14 ++++---- library/library.ml | 18 +++++----- library/library.mli | 14 ++++---- library/nameops.ml | 14 ++++---- library/nameops.mli | 14 ++++---- library/nametab.ml | 14 ++++---- library/nametab.mli | 14 ++++---- library/states.ml | 14 ++++---- library/states.mli | 14 ++++---- library/summary.ml | 14 ++++---- library/summary.mli | 14 ++++---- parsing/argextend.ml4 | 14 ++++---- parsing/ast.ml | 14 ++++---- parsing/ast.mli | 14 ++++---- parsing/coqast.ml | 14 ++++---- parsing/coqast.mli | 14 ++++---- parsing/egrammar.ml | 14 ++++---- parsing/egrammar.mli | 14 ++++---- parsing/esyntax.ml | 14 ++++---- parsing/esyntax.mli | 14 ++++---- parsing/extend.ml | 14 ++++---- parsing/extend.mli | 14 ++++---- parsing/g_basevernac.ml4 | 14 ++++---- parsing/g_cases.ml4 | 14 ++++---- parsing/g_constr.ml4 | 14 ++++---- parsing/g_constrnew.ml4 | 14 ++++---- parsing/g_ltac.ml4 | 14 ++++---- parsing/g_ltacnew.ml4 | 14 ++++---- parsing/g_minicoq.ml4 | 14 ++++---- parsing/g_minicoq.mli | 14 ++++---- parsing/g_module.ml4 | 14 ++++---- parsing/g_natsyntax.ml | 20 ++++++------ parsing/g_natsyntax.mli | 14 ++++---- parsing/g_natsyntaxnew.mli | 14 ++++---- parsing/g_prim.ml4 | 14 ++++---- parsing/g_primnew.ml4 | 14 ++++---- parsing/g_proofs.ml4 | 14 ++++---- parsing/g_proofsnew.ml4 | 14 ++++---- parsing/g_rsyntax.ml | 16 ++++----- parsing/g_tactic.ml4 | 14 ++++---- parsing/g_tacticnew.ml4 | 14 ++++---- parsing/g_vernac.ml4 | 14 ++++---- parsing/g_vernacnew.ml4 | 14 ++++---- parsing/g_zsyntax.ml | 24 +++++++------- parsing/g_zsyntax.mli | 14 ++++---- parsing/g_zsyntaxnew.mli | 14 ++++---- parsing/lexer.ml4 | 14 ++++---- parsing/lexer.mli | 14 ++++---- parsing/pcoq.ml4 | 14 ++++---- parsing/pcoq.mli | 14 ++++---- parsing/ppconstr.ml | 14 ++++---- parsing/ppconstr.mli | 14 ++++---- parsing/pptactic.ml | 14 ++++---- parsing/pptactic.mli | 14 ++++---- parsing/prettyp.ml | 14 ++++---- parsing/prettyp.mli | 14 ++++---- parsing/printer.ml | 14 ++++---- parsing/printer.mli | 14 ++++---- parsing/printmod.ml | 14 ++++---- parsing/printmod.mli | 14 ++++---- parsing/q_coqast.ml4 | 14 ++++---- parsing/q_util.ml4 | 14 ++++---- parsing/q_util.mli | 14 ++++---- parsing/search.ml | 14 ++++---- parsing/search.mli | 14 ++++---- parsing/tacextend.ml4 | 14 ++++---- parsing/termast.ml | 14 ++++---- parsing/termast.mli | 14 ++++---- parsing/vernacextend.ml4 | 14 ++++---- pretyping/cases.ml | 16 ++++----- pretyping/cases.mli | 14 ++++---- pretyping/cbv.ml | 14 ++++---- pretyping/cbv.mli | 18 +++++----- pretyping/classops.ml | 14 ++++---- pretyping/classops.mli | 14 ++++---- pretyping/coercion.ml | 14 ++++---- pretyping/coercion.mli | 14 ++++---- pretyping/detyping.ml | 14 ++++---- pretyping/detyping.mli | 14 ++++---- pretyping/evarconv.ml | 14 ++++---- pretyping/evarconv.mli | 14 ++++---- pretyping/evarutil.ml | 14 ++++---- pretyping/evarutil.mli | 14 ++++---- pretyping/evd.ml | 14 ++++---- pretyping/evd.mli | 14 ++++---- pretyping/indrec.ml | 14 ++++---- pretyping/indrec.mli | 14 ++++---- pretyping/inductiveops.ml | 14 ++++---- pretyping/inductiveops.mli | 14 ++++---- pretyping/instantiate.ml | 14 ++++---- pretyping/instantiate.mli | 14 ++++---- pretyping/matching.ml | 14 ++++---- pretyping/matching.mli | 14 ++++---- pretyping/pattern.ml | 14 ++++---- pretyping/pattern.mli | 14 ++++---- pretyping/pretype_errors.ml | 14 ++++---- pretyping/pretype_errors.mli | 14 ++++---- pretyping/pretyping.ml | 18 +++++----- pretyping/pretyping.mli | 14 ++++---- pretyping/rawterm.ml | 14 ++++---- pretyping/rawterm.mli | 14 ++++---- pretyping/recordops.ml | 14 ++++---- pretyping/recordops.mli | 14 ++++---- pretyping/reductionops.ml | 14 ++++---- pretyping/reductionops.mli | 14 ++++---- pretyping/retyping.ml | 14 ++++---- pretyping/retyping.mli | 14 ++++---- pretyping/tacred.ml | 16 ++++----- pretyping/tacred.mli | 14 ++++---- pretyping/termops.ml | 14 ++++---- pretyping/termops.mli | 14 ++++---- pretyping/typing.ml | 14 ++++---- pretyping/typing.mli | 14 ++++---- proofs/clenv.ml | 14 ++++---- proofs/clenv.mli | 14 ++++---- proofs/evar_refiner.ml | 14 ++++---- proofs/evar_refiner.mli | 14 ++++---- proofs/logic.ml | 30 ++++++++--------- proofs/logic.mli | 14 ++++---- proofs/pfedit.ml | 14 ++++---- proofs/pfedit.mli | 14 ++++---- proofs/proof_trees.ml | 14 ++++---- proofs/proof_trees.mli | 14 ++++---- proofs/proof_type.ml | 14 ++++---- proofs/proof_type.mli | 14 ++++---- proofs/refiner.ml | 14 ++++---- proofs/refiner.mli | 14 ++++---- proofs/tacexpr.ml | 14 ++++---- proofs/tacmach.ml | 14 ++++---- proofs/tacmach.mli | 14 ++++---- proofs/tactic_debug.ml | 14 ++++---- proofs/tactic_debug.mli | 14 ++++---- scripts/coqc.ml | 14 ++++---- scripts/coqmktop.ml | 14 ++++---- states/MakeInitial.v | 14 ++++---- states/MakeInitialNew.v | 14 ++++---- states7/MakeInitial.v | 14 ++++---- syntax/MakeBare.v | 14 ++++---- syntax/PPCases.v | 14 ++++---- syntax/PPConstr.v | 14 ++++---- tactics/auto.ml | 14 ++++---- tactics/auto.mli | 14 ++++---- tactics/autorewrite.ml | 14 ++++---- tactics/autorewrite.mli | 14 ++++---- tactics/btermdn.ml | 14 ++++---- tactics/btermdn.mli | 14 ++++---- tactics/contradiction.ml | 14 ++++---- tactics/contradiction.mli | 14 ++++---- tactics/dhyp.ml | 14 ++++---- tactics/dhyp.mli | 14 ++++---- tactics/dn.ml | 14 ++++---- tactics/dn.mli | 14 ++++---- tactics/eauto.ml4 | 14 ++++---- tactics/eauto.mli | 14 ++++---- tactics/elim.ml | 14 ++++---- tactics/elim.mli | 14 ++++---- tactics/eqdecide.ml4 | 20 ++++++------ tactics/equality.ml | 14 ++++---- tactics/equality.mli | 14 ++++---- tactics/evar_tactics.ml | 14 ++++---- tactics/evar_tactics.mli | 14 ++++---- tactics/extraargs.ml4 | 14 ++++---- tactics/extraargs.mli | 14 ++++---- tactics/extratactics.ml4 | 14 ++++---- tactics/extratactics.mli | 14 ++++---- tactics/hiddentac.ml | 14 ++++---- tactics/hiddentac.mli | 14 ++++---- tactics/hipattern.ml | 14 ++++---- tactics/hipattern.mli | 14 ++++---- tactics/inv.ml | 14 ++++---- tactics/inv.mli | 14 ++++---- tactics/leminv.ml | 14 ++++---- tactics/nbtermdn.ml | 14 ++++---- tactics/nbtermdn.mli | 14 ++++---- tactics/refine.ml | 14 ++++---- tactics/refine.mli | 14 ++++---- tactics/setoid_replace.ml | 14 ++++---- tactics/setoid_replace.mli | 14 ++++---- tactics/tacinterp.ml | 14 ++++---- tactics/tacinterp.mli | 14 ++++---- tactics/tacticals.ml | 14 ++++---- tactics/tacticals.mli | 14 ++++---- tactics/tactics.ml | 14 ++++---- tactics/tactics.mli | 14 ++++---- tactics/tauto.ml4 | 14 ++++---- tactics/termdn.ml | 14 ++++---- tactics/termdn.mli | 14 ++++---- test-suite/bench/lists-100.v | 14 ++++---- test-suite/bench/lists_100.v | 14 ++++---- test-suite/failure/Tauto.v | 14 ++++---- test-suite/failure/clash_cons.v | 14 ++++---- test-suite/failure/fixpoint1.v | 14 ++++---- test-suite/failure/illtype1.v | 14 ++++---- test-suite/failure/positivity.v | 14 ++++---- test-suite/failure/redef.v | 14 ++++---- test-suite/failure/search.v | 14 ++++---- test-suite/ideal-features/Apply.v | 14 ++++---- test-suite/success/Check.v | 14 ++++---- test-suite/success/Field.v | 14 ++++---- test-suite/success/Tauto.v | 14 ++++---- test-suite/success/eauto.v | 14 ++++---- test-suite/success/eqdecide.v | 14 ++++---- test-suite/success/fix.v | 14 ++++---- test-suite/success/import_lib.v | 4 +-- test-suite/success/inds_type_sec.v | 14 ++++---- test-suite/success/induct.v | 14 ++++---- test-suite/success/mutual_ind.v | 14 ++++---- test-suite/success/unfold.v | 14 ++++---- test-suite/tactics/TestRefine.v | 26 +++++++-------- theories/Arith/Arith.v | 14 ++++---- theories/Arith/Between.v | 14 ++++---- theories/Arith/Bool_nat.v | 14 ++++---- theories/Arith/Compare.v | 14 ++++---- theories/Arith/Compare_dec.v | 14 ++++---- theories/Arith/Div.v | 14 ++++---- theories/Arith/Div2.v | 14 ++++---- theories/Arith/EqNat.v | 14 ++++---- theories/Arith/Euclid.v | 14 ++++---- theories/Arith/Even.v | 14 ++++---- theories/Arith/Factorial.v | 14 ++++---- theories/Arith/Gt.v | 14 ++++---- theories/Arith/Le.v | 14 ++++---- theories/Arith/Lt.v | 14 ++++---- theories/Arith/Max.v | 14 ++++---- theories/Arith/Min.v | 14 ++++---- theories/Arith/Minus.v | 14 ++++---- theories/Arith/Mult.v | 14 ++++---- theories/Arith/Peano_dec.v | 14 ++++---- theories/Arith/Plus.v | 14 ++++---- theories/Arith/Wf_nat.v | 14 ++++---- theories/Bool/Bool.v | 14 ++++---- theories/Bool/BoolEq.v | 14 ++++---- theories/Bool/Bvector.v | 14 ++++---- theories/Bool/DecBool.v | 14 ++++---- theories/Bool/IfProp.v | 14 ++++---- theories/Bool/Sumbool.v | 14 ++++---- theories/Bool/Zerob.v | 14 ++++---- theories/Init/Datatypes.v | 14 ++++---- theories/Init/Logic.v | 14 ++++---- theories/Init/Logic_Type.v | 14 ++++---- theories/Init/Notations.v | 14 ++++---- theories/Init/Peano.v | 14 ++++---- theories/Init/Prelude.v | 14 ++++---- theories/Init/Specif.v | 14 ++++---- theories/Init/Wf.v | 14 ++++---- theories/IntMap/Adalloc.v | 14 ++++---- theories/IntMap/Addec.v | 14 ++++---- theories/IntMap/Addr.v | 14 ++++---- theories/IntMap/Adist.v | 14 ++++---- theories/IntMap/Allmaps.v | 14 ++++---- theories/IntMap/Fset.v | 14 ++++---- theories/IntMap/Lsort.v | 14 ++++---- theories/IntMap/Map.v | 14 ++++---- theories/IntMap/Mapaxioms.v | 14 ++++---- theories/IntMap/Mapc.v | 14 ++++---- theories/IntMap/Mapcanon.v | 14 ++++---- theories/IntMap/Mapcard.v | 14 ++++---- theories/IntMap/Mapfold.v | 14 ++++---- theories/IntMap/Mapiter.v | 14 ++++---- theories/IntMap/Maplists.v | 14 ++++---- theories/IntMap/Mapsubset.v | 14 ++++---- theories/Lists/List.v | 14 ++++---- theories/Lists/ListSet.v | 14 ++++---- theories/Lists/MonoList.v | 14 ++++---- theories/Lists/Streams.v | 14 ++++---- theories/Lists/TheoryList.v | 14 ++++---- theories/Logic/Berardi.v | 14 ++++---- theories/Logic/ChoiceFacts.v | 14 ++++---- theories/Logic/Classical.v | 14 ++++---- theories/Logic/ClassicalChoice.v | 14 ++++---- theories/Logic/ClassicalDescription.v | 14 ++++---- theories/Logic/ClassicalFacts.v | 14 ++++---- theories/Logic/Classical_Pred_Set.v | 14 ++++---- theories/Logic/Classical_Pred_Type.v | 14 ++++---- theories/Logic/Classical_Prop.v | 14 ++++---- theories/Logic/Classical_Type.v | 14 ++++---- theories/Logic/Decidable.v | 14 ++++---- theories/Logic/Diaconescu.v | 14 ++++---- theories/Logic/Eqdep.v | 14 ++++---- theories/Logic/Eqdep_dec.v | 14 ++++---- theories/Logic/Hurkens.v | 24 ++++++-------- theories/Logic/JMeq.v | 14 ++++---- theories/Logic/ProofIrrelevance.v | 18 ++++------ theories/Logic/RelationalChoice.v | 14 ++++---- theories/NArith/BinNat.v | 14 ++++---- theories/NArith/BinPos.v | 14 ++++---- theories/NArith/NArith.v | 14 ++++---- theories/NArith/Pnat.v | 14 ++++---- theories/Num/AddProps.v | 14 ++++---- theories/Num/Axioms.v | 14 ++++---- theories/Num/Definitions.v | 14 ++++---- theories/Num/DiscrAxioms.v | 14 ++++---- theories/Num/DiscrProps.v | 14 ++++---- theories/Num/EqAxioms.v | 14 ++++---- theories/Num/EqParams.v | 14 ++++---- theories/Num/GeAxioms.v | 14 ++++---- theories/Num/GeProps.v | 14 ++++---- theories/Num/GtAxioms.v | 14 ++++---- theories/Num/GtProps.v | 14 ++++---- theories/Num/LeAxioms.v | 14 ++++---- theories/Num/LeProps.v | 14 ++++---- theories/Num/LtProps.v | 14 ++++---- theories/Num/NSyntax.v | 14 ++++---- theories/Num/NeqAxioms.v | 14 ++++---- theories/Num/NeqDef.v | 14 ++++---- theories/Num/NeqParams.v | 14 ++++---- theories/Num/NeqProps.v | 14 ++++---- theories/Num/OppAxioms.v | 14 ++++---- theories/Num/OppProps.v | 14 ++++---- theories/Num/Params.v | 14 ++++---- theories/Num/SubProps.v | 14 ++++---- theories/Reals/Alembert.v | 14 ++++---- theories/Reals/AltSeries.v | 14 ++++---- theories/Reals/ArithProp.v | 14 ++++---- theories/Reals/Binomial.v | 14 ++++---- theories/Reals/Cauchy_prod.v | 14 ++++---- theories/Reals/Cos_plus.v | 14 ++++---- theories/Reals/Cos_rel.v | 14 ++++---- theories/Reals/DiscrR.v | 14 ++++---- theories/Reals/Exp_prop.v | 14 ++++---- theories/Reals/Integration.v | 14 ++++---- theories/Reals/MVT.v | 14 ++++---- theories/Reals/NewtonInt.v | 14 ++++---- theories/Reals/PSeries_reg.v | 14 ++++---- theories/Reals/PartSum.v | 14 ++++---- theories/Reals/RIneq.v | 14 ++++---- theories/Reals/RList.v | 14 ++++---- theories/Reals/R_Ifp.v | 14 ++++---- theories/Reals/R_sqr.v | 14 ++++---- theories/Reals/R_sqrt.v | 14 ++++---- theories/Reals/Ranalysis.v | 14 ++++---- theories/Reals/Ranalysis1.v | 14 ++++---- theories/Reals/Ranalysis2.v | 14 ++++---- theories/Reals/Ranalysis3.v | 14 ++++---- theories/Reals/Ranalysis4.v | 14 ++++---- theories/Reals/Raxioms.v | 14 ++++---- theories/Reals/Rbase.v | 14 ++++---- theories/Reals/Rbasic_fun.v | 14 ++++---- theories/Reals/Rcomplete.v | 14 ++++---- theories/Reals/Rdefinitions.v | 14 ++++---- theories/Reals/Rderiv.v | 14 ++++---- theories/Reals/Reals.v | 14 ++++---- theories/Reals/Rfunctions.v | 14 ++++---- theories/Reals/Rgeom.v | 14 ++++---- theories/Reals/RiemannInt.v | 14 ++++---- theories/Reals/RiemannInt_SF.v | 14 ++++---- theories/Reals/Rlimit.v | 14 ++++---- theories/Reals/Rpower.v | 14 ++++---- theories/Reals/Rprod.v | 14 ++++---- theories/Reals/Rseries.v | 14 ++++---- theories/Reals/Rsigma.v | 14 ++++---- theories/Reals/Rsqrt_def.v | 14 ++++---- theories/Reals/Rtopology.v | 14 ++++---- theories/Reals/Rtrigo.v | 14 ++++---- theories/Reals/Rtrigo_alt.v | 14 ++++---- theories/Reals/Rtrigo_calc.v | 14 ++++---- theories/Reals/Rtrigo_def.v | 14 ++++---- theories/Reals/Rtrigo_fun.v | 14 ++++---- theories/Reals/Rtrigo_reg.v | 14 ++++---- theories/Reals/SeqProp.v | 14 ++++---- theories/Reals/SeqSeries.v | 14 ++++---- theories/Reals/SplitAbsolu.v | 14 ++++---- theories/Reals/SplitRmult.v | 14 ++++---- theories/Reals/Sqrt_reg.v | 14 ++++---- theories/Relations/Newman.v | 14 ++++---- theories/Relations/Operators_Properties.v | 14 ++++---- theories/Relations/Relation_Definitions.v | 14 ++++---- theories/Relations/Relation_Operators.v | 14 ++++---- theories/Relations/Relations.v | 14 ++++---- theories/Relations/Rstar.v | 14 ++++---- theories/Setoids/Setoid.v | 14 ++++---- theories/Sets/Classical_sets.v | 14 ++++---- theories/Sets/Constructive_sets.v | 14 ++++---- theories/Sets/Cpo.v | 14 ++++---- theories/Sets/Ensembles.v | 14 ++++---- theories/Sets/Finite_sets.v | 14 ++++---- theories/Sets/Finite_sets_facts.v | 14 ++++---- theories/Sets/Image.v | 14 ++++---- theories/Sets/Infinite_sets.v | 14 ++++---- theories/Sets/Integers.v | 14 ++++---- theories/Sets/Multiset.v | 14 ++++---- theories/Sets/Partial_Order.v | 14 ++++---- theories/Sets/Permut.v | 14 ++++---- theories/Sets/Powerset.v | 14 ++++---- theories/Sets/Powerset_Classical_facts.v | 14 ++++---- theories/Sets/Powerset_facts.v | 14 ++++---- theories/Sets/Relations_1.v | 14 ++++---- theories/Sets/Relations_1_facts.v | 14 ++++---- theories/Sets/Relations_2.v | 14 ++++---- theories/Sets/Relations_2_facts.v | 14 ++++---- theories/Sets/Relations_3.v | 14 ++++---- theories/Sets/Relations_3_facts.v | 14 ++++---- theories/Sets/Uniset.v | 14 ++++---- theories/Sorting/Heap.v | 14 ++++---- theories/Sorting/Permutation.v | 14 ++++---- theories/Sorting/Sorting.v | 14 ++++---- theories/Wellfounded/Disjoint_Union.v | 14 ++++---- theories/Wellfounded/Inclusion.v | 14 ++++---- theories/Wellfounded/Inverse_Image.v | 14 ++++---- .../Wellfounded/Lexicographic_Exponentiation.v | 14 ++++---- theories/Wellfounded/Lexicographic_Product.v | 14 ++++---- theories/Wellfounded/Transitive_Closure.v | 14 ++++---- theories/Wellfounded/Union.v | 14 ++++---- theories/Wellfounded/Well_Ordering.v | 14 ++++---- theories/Wellfounded/Wellfounded.v | 14 ++++---- theories/ZArith/BinInt.v | 14 ++++---- theories/ZArith/Wf_Z.v | 14 ++++---- theories/ZArith/ZArith.v | 14 ++++---- theories/ZArith/ZArith_base.v | 14 ++++---- theories/ZArith/ZArith_dec.v | 14 ++++---- theories/ZArith/Zabs.v | 14 ++++---- theories/ZArith/Zbinary.v | 14 ++++---- theories/ZArith/Zbool.v | 14 ++++---- theories/ZArith/Zcompare.v | 14 ++++---- theories/ZArith/Zcomplements.v | 14 ++++---- theories/ZArith/Zdiv.v | 14 ++++---- theories/ZArith/Zeven.v | 14 ++++---- theories/ZArith/Zhints.v | 14 ++++---- theories/ZArith/Zlogarithm.v | 14 ++++---- theories/ZArith/Zmin.v | 14 ++++---- theories/ZArith/Zmisc.v | 14 ++++---- theories/ZArith/Znat.v | 14 ++++---- theories/ZArith/Znumtheory.v | 14 ++++---- theories/ZArith/Zorder.v | 14 ++++---- theories/ZArith/Zpower.v | 14 ++++---- theories/ZArith/Zsqrt.v | 14 ++++---- theories/ZArith/Zwf.v | 14 ++++---- theories/ZArith/auxiliary.v | 14 ++++---- theories7/Arith/Arith.v | 14 ++++---- theories7/Arith/Between.v | 14 ++++---- theories7/Arith/Bool_nat.v | 14 ++++---- theories7/Arith/Compare.v | 14 ++++---- theories7/Arith/Compare_dec.v | 14 ++++---- theories7/Arith/Div.v | 14 ++++---- theories7/Arith/Div2.v | 14 ++++---- theories7/Arith/EqNat.v | 14 ++++---- theories7/Arith/Euclid.v | 14 ++++---- theories7/Arith/Even.v | 14 ++++---- theories7/Arith/Factorial.v | 14 ++++---- theories7/Arith/Gt.v | 14 ++++---- theories7/Arith/Le.v | 14 ++++---- theories7/Arith/Lt.v | 14 ++++---- theories7/Arith/Max.v | 14 ++++---- theories7/Arith/Min.v | 14 ++++---- theories7/Arith/Minus.v | 14 ++++---- theories7/Arith/Mult.v | 14 ++++---- theories7/Arith/Peano_dec.v | 14 ++++---- theories7/Arith/Plus.v | 14 ++++---- theories7/Arith/Wf_nat.v | 14 ++++---- theories7/Bool/Bool.v | 14 ++++---- theories7/Bool/BoolEq.v | 14 ++++---- theories7/Bool/Bvector.v | 14 ++++---- theories7/Bool/DecBool.v | 14 ++++---- theories7/Bool/IfProp.v | 14 ++++---- theories7/Bool/Sumbool.v | 14 ++++---- theories7/Bool/Zerob.v | 14 ++++---- theories7/Init/Datatypes.v | 14 ++++---- theories7/Init/Logic.v | 14 ++++---- theories7/Init/Logic_Type.v | 14 ++++---- theories7/Init/Notations.v | 14 ++++---- theories7/Init/Peano.v | 14 ++++---- theories7/Init/Prelude.v | 14 ++++---- theories7/Init/Specif.v | 14 ++++---- theories7/Init/Wf.v | 14 ++++---- theories7/IntMap/Adalloc.v | 14 ++++---- theories7/IntMap/Addec.v | 14 ++++---- theories7/IntMap/Addr.v | 14 ++++---- theories7/IntMap/Adist.v | 14 ++++---- theories7/IntMap/Allmaps.v | 14 ++++---- theories7/IntMap/Fset.v | 14 ++++---- theories7/IntMap/Lsort.v | 14 ++++---- theories7/IntMap/Map.v | 14 ++++---- theories7/IntMap/Mapaxioms.v | 14 ++++---- theories7/IntMap/Mapc.v | 14 ++++---- theories7/IntMap/Mapcanon.v | 14 ++++---- theories7/IntMap/Mapcard.v | 14 ++++---- theories7/IntMap/Mapfold.v | 14 ++++---- theories7/IntMap/Mapiter.v | 14 ++++---- theories7/IntMap/Maplists.v | 14 ++++---- theories7/IntMap/Mapsubset.v | 14 ++++---- theories7/Lists/List.v | 14 ++++---- theories7/Lists/ListSet.v | 14 ++++---- theories7/Lists/MonoList.v | 14 ++++---- theories7/Lists/PolyList.v | 14 ++++---- theories7/Lists/PolyListSyntax.v | 14 ++++---- theories7/Lists/Streams.v | 14 ++++---- theories7/Lists/TheoryList.v | 14 ++++---- theories7/Logic/Berardi.v | 14 ++++---- theories7/Logic/ChoiceFacts.v | 14 ++++---- theories7/Logic/Classical.v | 14 ++++---- theories7/Logic/ClassicalChoice.v | 14 ++++---- theories7/Logic/ClassicalDescription.v | 14 ++++---- theories7/Logic/ClassicalFacts.v | 14 ++++---- theories7/Logic/Classical_Pred_Set.v | 14 ++++---- theories7/Logic/Classical_Pred_Type.v | 14 ++++---- theories7/Logic/Classical_Prop.v | 14 ++++---- theories7/Logic/Classical_Type.v | 14 ++++---- theories7/Logic/Decidable.v | 14 ++++---- theories7/Logic/Diaconescu.v | 14 ++++---- theories7/Logic/Eqdep.v | 14 ++++---- theories7/Logic/Eqdep_dec.v | 14 ++++---- theories7/Logic/Hurkens.v | 22 +++++-------- theories7/Logic/JMeq.v | 14 ++++---- theories7/Logic/ProofIrrelevance.v | 18 ++++------ theories7/Logic/RelationalChoice.v | 14 ++++---- theories7/NArith/BinNat.v | 14 ++++---- theories7/NArith/BinPos.v | 14 ++++---- theories7/NArith/NArith.v | 14 ++++---- theories7/NArith/Pnat.v | 14 ++++---- theories7/Reals/Alembert.v | 14 ++++---- theories7/Reals/AltSeries.v | 14 ++++---- theories7/Reals/ArithProp.v | 14 ++++---- theories7/Reals/Binomial.v | 14 ++++---- theories7/Reals/Cauchy_prod.v | 14 ++++---- theories7/Reals/Cos_plus.v | 14 ++++---- theories7/Reals/Cos_rel.v | 14 ++++---- theories7/Reals/DiscrR.v | 14 ++++---- theories7/Reals/Exp_prop.v | 14 ++++---- theories7/Reals/Integration.v | 14 ++++---- theories7/Reals/MVT.v | 14 ++++---- theories7/Reals/NewtonInt.v | 14 ++++---- theories7/Reals/PSeries_reg.v | 14 ++++---- theories7/Reals/PartSum.v | 14 ++++---- theories7/Reals/RIneq.v | 14 ++++---- theories7/Reals/RList.v | 14 ++++---- theories7/Reals/R_Ifp.v | 14 ++++---- theories7/Reals/R_sqr.v | 14 ++++---- theories7/Reals/R_sqrt.v | 14 ++++---- theories7/Reals/Ranalysis.v | 14 ++++---- theories7/Reals/Ranalysis1.v | 14 ++++---- theories7/Reals/Ranalysis2.v | 14 ++++---- theories7/Reals/Ranalysis3.v | 14 ++++---- theories7/Reals/Ranalysis4.v | 14 ++++---- theories7/Reals/Raxioms.v | 14 ++++---- theories7/Reals/Rbase.v | 14 ++++---- theories7/Reals/Rbasic_fun.v | 14 ++++---- theories7/Reals/Rcomplete.v | 14 ++++---- theories7/Reals/Rdefinitions.v | 14 ++++---- theories7/Reals/Rderiv.v | 14 ++++---- theories7/Reals/Reals.v | 14 ++++---- theories7/Reals/Rfunctions.v | 14 ++++---- theories7/Reals/Rgeom.v | 14 ++++---- theories7/Reals/RiemannInt.v | 14 ++++---- theories7/Reals/RiemannInt_SF.v | 14 ++++---- theories7/Reals/Rlimit.v | 14 ++++---- theories7/Reals/Rpower.v | 14 ++++---- theories7/Reals/Rprod.v | 14 ++++---- theories7/Reals/Rseries.v | 14 ++++---- theories7/Reals/Rsigma.v | 14 ++++---- theories7/Reals/Rsqrt_def.v | 14 ++++---- theories7/Reals/Rsyntax.v | 14 ++++---- theories7/Reals/Rtopology.v | 14 ++++---- theories7/Reals/Rtrigo.v | 14 ++++---- theories7/Reals/Rtrigo_alt.v | 14 ++++---- theories7/Reals/Rtrigo_calc.v | 14 ++++---- theories7/Reals/Rtrigo_def.v | 14 ++++---- theories7/Reals/Rtrigo_fun.v | 14 ++++---- theories7/Reals/Rtrigo_reg.v | 14 ++++---- theories7/Reals/SeqProp.v | 14 ++++---- theories7/Reals/SeqSeries.v | 14 ++++---- theories7/Reals/SplitAbsolu.v | 14 ++++---- theories7/Reals/SplitRmult.v | 14 ++++---- theories7/Reals/Sqrt_reg.v | 14 ++++---- theories7/Relations/Newman.v | 14 ++++---- theories7/Relations/Operators_Properties.v | 14 ++++---- theories7/Relations/Relation_Definitions.v | 14 ++++---- theories7/Relations/Relation_Operators.v | 14 ++++---- theories7/Relations/Relations.v | 14 ++++---- theories7/Relations/Rstar.v | 14 ++++---- theories7/Setoids/Setoid.v | 14 ++++---- theories7/Sets/Classical_sets.v | 14 ++++---- theories7/Sets/Constructive_sets.v | 14 ++++---- theories7/Sets/Cpo.v | 14 ++++---- theories7/Sets/Ensembles.v | 14 ++++---- theories7/Sets/Finite_sets.v | 14 ++++---- theories7/Sets/Finite_sets_facts.v | 14 ++++---- theories7/Sets/Image.v | 14 ++++---- theories7/Sets/Infinite_sets.v | 14 ++++---- theories7/Sets/Integers.v | 14 ++++---- theories7/Sets/Multiset.v | 14 ++++---- theories7/Sets/Partial_Order.v | 14 ++++---- theories7/Sets/Permut.v | 14 ++++---- theories7/Sets/Powerset.v | 14 ++++---- theories7/Sets/Powerset_Classical_facts.v | 14 ++++---- theories7/Sets/Powerset_facts.v | 14 ++++---- theories7/Sets/Relations_1.v | 14 ++++---- theories7/Sets/Relations_1_facts.v | 14 ++++---- theories7/Sets/Relations_2.v | 14 ++++---- theories7/Sets/Relations_2_facts.v | 14 ++++---- theories7/Sets/Relations_3.v | 14 ++++---- theories7/Sets/Relations_3_facts.v | 14 ++++---- theories7/Sets/Uniset.v | 14 ++++---- theories7/Sorting/Heap.v | 14 ++++---- theories7/Sorting/Permutation.v | 14 ++++---- theories7/Sorting/Sorting.v | 14 ++++---- theories7/Wellfounded/Disjoint_Union.v | 14 ++++---- theories7/Wellfounded/Inclusion.v | 14 ++++---- theories7/Wellfounded/Inverse_Image.v | 14 ++++---- .../Wellfounded/Lexicographic_Exponentiation.v | 14 ++++---- theories7/Wellfounded/Lexicographic_Product.v | 14 ++++---- theories7/Wellfounded/Transitive_Closure.v | 14 ++++---- theories7/Wellfounded/Union.v | 14 ++++---- theories7/Wellfounded/Well_Ordering.v | 14 ++++---- theories7/Wellfounded/Wellfounded.v | 14 ++++---- theories7/ZArith/BinInt.v | 14 ++++---- theories7/ZArith/Wf_Z.v | 14 ++++---- theories7/ZArith/ZArith.v | 14 ++++---- theories7/ZArith/ZArith_base.v | 14 ++++---- theories7/ZArith/ZArith_dec.v | 14 ++++---- theories7/ZArith/Zabs.v | 14 ++++---- theories7/ZArith/Zbinary.v | 14 ++++---- theories7/ZArith/Zbool.v | 14 ++++---- theories7/ZArith/Zcompare.v | 14 ++++---- theories7/ZArith/Zcomplements.v | 14 ++++---- theories7/ZArith/Zdiv.v | 14 ++++---- theories7/ZArith/Zeven.v | 14 ++++---- theories7/ZArith/Zhints.v | 14 ++++---- theories7/ZArith/Zlogarithm.v | 14 ++++---- theories7/ZArith/Zmin.v | 14 ++++---- theories7/ZArith/Zmisc.v | 14 ++++---- theories7/ZArith/Znat.v | 14 ++++---- theories7/ZArith/Znumtheory.v | 14 ++++---- theories7/ZArith/Zorder.v | 14 ++++---- theories7/ZArith/Zpower.v | 14 ++++---- theories7/ZArith/Zsqrt.v | 14 ++++---- theories7/ZArith/Zsyntax.v | 14 ++++---- theories7/ZArith/Zwf.v | 14 ++++---- theories7/ZArith/auxiliary.v | 14 ++++---- theories7/ZArith/fast_integer.v | 14 ++++---- theories7/ZArith/zarith_aux.v | 14 ++++---- tools/coq-tex.ml4 | 14 ++++---- tools/coq_makefile.ml4 | 14 ++++---- tools/coqdep.ml | 14 ++++---- tools/coqdep_lexer.mll | 14 ++++---- tools/coqdoc/alpha.ml | 14 ++++---- tools/coqdoc/alpha.mli | 14 ++++---- tools/coqdoc/index.mli | 14 ++++---- tools/coqdoc/index.mll | 14 ++++---- tools/coqdoc/main.ml | 14 ++++---- tools/coqdoc/output.ml | 14 ++++---- tools/coqdoc/output.mli | 14 ++++---- tools/coqdoc/pretty.mli | 14 ++++---- tools/coqdoc/pretty.mll | 14 ++++---- tools/coqwc.mll | 14 ++++---- tools/gallina.ml | 14 ++++---- tools/gallina_lexer.mll | 14 ++++---- toplevel/cerrors.ml | 14 ++++---- toplevel/cerrors.mli | 14 ++++---- toplevel/class.ml | 14 ++++---- toplevel/class.mli | 14 ++++---- toplevel/command.ml | 14 ++++---- toplevel/command.mli | 14 ++++---- toplevel/coqinit.ml | 14 ++++---- toplevel/coqinit.mli | 14 ++++---- toplevel/coqtop.ml | 14 ++++---- toplevel/coqtop.mli | 14 ++++---- toplevel/discharge.ml | 14 ++++---- toplevel/discharge.mli | 14 ++++---- toplevel/fhimsg.ml | 14 ++++---- toplevel/fhimsg.mli | 14 ++++---- toplevel/himsg.ml | 14 ++++---- toplevel/himsg.mli | 14 ++++---- toplevel/line_oriented_parser.ml | 14 ++++---- toplevel/line_oriented_parser.mli | 14 ++++---- toplevel/metasyntax.ml | 14 ++++---- toplevel/metasyntax.mli | 14 ++++---- toplevel/minicoq.ml | 14 ++++---- toplevel/mltop.ml4 | 14 ++++---- toplevel/mltop.mli | 14 ++++---- toplevel/protectedtoplevel.ml | 14 ++++---- toplevel/protectedtoplevel.mli | 14 ++++---- toplevel/record.ml | 14 ++++---- toplevel/record.mli | 14 ++++---- toplevel/recordobj.ml | 14 ++++---- toplevel/recordobj.mli | 14 ++++---- toplevel/searchisos.mli | 14 ++++---- toplevel/toplevel.ml | 14 ++++---- toplevel/toplevel.mli | 14 ++++---- toplevel/usage.ml | 14 ++++---- toplevel/usage.mli | 14 ++++---- toplevel/vernac.ml | 14 ++++---- toplevel/vernac.mli | 14 ++++---- toplevel/vernacentries.ml | 14 ++++---- toplevel/vernacentries.mli | 14 ++++---- toplevel/vernacexpr.ml | 14 ++++---- toplevel/vernacinterp.ml | 14 ++++---- toplevel/vernacinterp.mli | 14 ++++---- translate/ppconstrnew.ml | 14 ++++---- translate/ppconstrnew.mli | 14 ++++---- translate/pptacticnew.ml | 14 ++++---- translate/pptacticnew.mli | 14 ++++---- translate/ppvernacnew.ml | 14 ++++---- translate/ppvernacnew.mli | 14 ++++---- 1004 files changed, 7172 insertions(+), 7188 deletions(-) diff --git a/config/coq_config.mli b/config/coq_config.mli index 7482a45c9..6adeaa705 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* reds -(***********************************************************************) +(************************************************************************) type table_key = | ConstKey of constant @@ -95,7 +95,7 @@ val ref_value_cache: 'a infos -> table_key -> 'a option val info_flags: 'a infos -> reds val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos -(***********************************************************************) +(************************************************************************) (*s A [stack] is a context of arguments, arguments are pushed by [append_stack] one array at a time but popped with [decomp_stack] one by one *) @@ -121,7 +121,7 @@ val app_stack : constr * constr stack -> constr val stack_tail : int -> 'a stack -> 'a stack val stack_nth : 'a stack -> int -> 'a -(***********************************************************************) +(************************************************************************) (*s Lazy reduction. *) (* [fconstr] is the type of frozen constr *) @@ -185,7 +185,7 @@ val unfold_reference : clos_infos -> table_key -> fconstr option (* [mind_equiv] checks whether two mutual inductives are intentionally equal *) val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool -(***********************************************************************) +(************************************************************************) (*i This is for lazy debug *) val lift_fconstr : int -> fconstr -> fconstr diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 527030fb4..11d4435c2 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* engagement option (* is the local context empty *) val empty_context : env -> bool -(***********************************************************************) +(************************************************************************) (*s Context of de Bruijn variables (rel_context) *) val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env @@ -58,7 +58,7 @@ val evaluable_rel : int -> env -> bool val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a -(***********************************************************************) +(************************************************************************) (* Context of variables (section variables and goal assumptions) *) val push_named : named_declaration -> env -> env @@ -80,7 +80,7 @@ val reset_context : env -> env (* This forgets rel context and sets a new named context *) val reset_with_named_context : named_context -> env -> env -(***********************************************************************) +(************************************************************************) (*s Global constants *) (*s Add entries to global environment *) val add_constant : constant -> constant_body -> env -> env @@ -100,7 +100,7 @@ val constant_value : env -> constant -> constr val constant_type : env -> constant -> types val constant_opt_value : env -> constant -> constr option -(***********************************************************************) +(************************************************************************) (*s Inductive types *) val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env @@ -108,7 +108,7 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env (* raises [Not_found] if the required path is not found *) val lookup_mind : mutual_inductive -> env -> mutual_inductive_body -(***********************************************************************) +(************************************************************************) (*s Modules *) val add_modtype : kernel_name -> module_type_body -> env -> env @@ -118,14 +118,14 @@ val shallow_add_module : module_path -> module_body -> env -> env val lookup_module : module_path -> env -> module_body val lookup_modtype : kernel_name -> env -> module_type_body -(***********************************************************************) +(************************************************************************) (*s Universe constraints *) val set_universes : Univ.universes -> env -> env val add_constraints : Univ.constraints -> env -> env val set_engagement : engagement -> env -> env -(***********************************************************************) +(************************************************************************) (* Sets of referred section variables *) (* [global_vars_set env c] returns the list of [id]'s occurring as [VAR id] in [c] *) @@ -135,7 +135,7 @@ val vars_of_global : env -> constr -> identifier list val keep_hyps : env -> Idset.t -> section_context -(***********************************************************************) +(************************************************************************) (*s Unsafe judgments. We introduce here the pre-type of judgments, which is actually only a datatype to store a term with its type and the type of its type. *) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index a72f5a634..7662a2f8b 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* check_arity id ar) mie.mind_entry_inds -(***********************************************************************) -(***********************************************************************) +(************************************************************************) +(************************************************************************) (* Typing the arities and constructor types *) @@ -233,8 +233,8 @@ let typecheck_inductive env mie = ([],cst) in (env_arities, Array.of_list inds, cst) -(***********************************************************************) -(***********************************************************************) +(************************************************************************) +(************************************************************************) (* Positivity *) type ill_formed_ind = @@ -446,8 +446,8 @@ let check_positivity env_ar inds = Rtree.mk_rec (Array.mapi check_one inds) -(***********************************************************************) -(***********************************************************************) +(************************************************************************) +(************************************************************************) (* Build the inductive packet *) (* Elimination sorts *) @@ -536,8 +536,8 @@ let build_inductive env env_ar record finite inds recargs cst = mind_equiv = None; } -(***********************************************************************) -(***********************************************************************) +(************************************************************************) +(************************************************************************) let check_inductive env mie = (* First type-check the inductive definition *) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 4e0f9012c..bbfa47818 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (ind, l) | _ -> raise Not_found -(***********************************************************************) +(************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) (* inductives *) @@ -86,8 +86,8 @@ let full_constructor_instantiate (((mind,_),mib,mip),params) = (fun t -> instantiate_params (inst_ind t) params mip.mind_params_ctxt) -(***********************************************************************) -(***********************************************************************) +(************************************************************************) +(************************************************************************) (* Functions to build standard types related to inductive *) @@ -97,7 +97,7 @@ let type_of_inductive env i = let (_,mip) = lookup_mind_specif env i in mip.mind_user_arity -(***********************************************************************) +(************************************************************************) (* Type of a constructor *) let type_of_constructor env cstr = @@ -118,7 +118,7 @@ let arities_of_constructors env ind = -(***********************************************************************) +(************************************************************************) let is_info_arity env c = match dest_arity env c with @@ -214,7 +214,7 @@ let is_correct_arity env c pj ind mip params = error_elim_arity env ind listarity c pj kinds -(***********************************************************************) +(************************************************************************) (* Type of case branches *) (* [p] is the predicate, [i] is the constructor number (starting from 0), @@ -254,7 +254,7 @@ let type_case_branches env (ind,largs) pj c = (lc, ty, univ) -(***********************************************************************) +(************************************************************************) (* Checking the case annotation is relevent *) let check_case_info env indsp ci = @@ -264,8 +264,8 @@ let check_case_info env indsp ci = (mip.mind_nparams <> ci.ci_npar) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) -(***********************************************************************) -(***********************************************************************) +(************************************************************************) +(************************************************************************) (* Guard conditions for fix and cofix-points *) @@ -510,7 +510,7 @@ let check_is_subterm renv c ind = Subterm (Strict,_) | Dead_code -> true | _ -> false -(***********************************************************************) +(************************************************************************) exception FixGuardError of env * guard_error @@ -711,7 +711,7 @@ let cfkey = Profile.declare_profile "check_fix";; let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; *) -(***********************************************************************) +(************************************************************************) (* Scrape *) let rec scrape_mind env kn = @@ -719,7 +719,7 @@ let rec scrape_mind env kn = | None -> kn | Some kn' -> scrape_mind env kn' -(***********************************************************************) +(************************************************************************) (* Co-fixpoints. *) exception CoFixGuardError of env * guard_error diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a6ce7d42e..0ecfe2a8c 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> constr @@ -22,7 +22,7 @@ val whd_betadeltaiota_nolet : env -> constr -> constr val nf_betaiota : constr -> constr -(***********************************************************************) +(************************************************************************) (*s conversion functions *) exception NotConvertible @@ -36,7 +36,7 @@ val conv : types conversion_function val conv_leq : types conversion_function val conv_leq_vecti : types array conversion_function -(***********************************************************************) +(************************************************************************) (* Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr @@ -45,7 +45,7 @@ val beta_appvect : constr -> constr array -> constr val hnf_prod_applist : env -> types -> constr list -> types -(***********************************************************************) +(************************************************************************) (*s Recognizing products and arities modulo reduction *) val dest_prod : env -> types -> Sign.rel_context * types diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d007af08e..0182b3907 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* error_ill_typed_rec_body env i lna vdefj lar -(***********************************************************************) -(***********************************************************************) +(************************************************************************) +(************************************************************************) (* This combinator adds the universe constraints both in the local graph and in the universes of the environment. This is to ensure diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 55adf86a2..a537d793e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* None -(***********************************************************************) +(************************************************************************) (* Declare the primitive parsers and printers *) let _ = @@ -193,7 +193,7 @@ let _ = (nat_of_int,Some pat_nat_of_int) ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, None) -(***********************************************************************) +(************************************************************************) (* Old ast printing *) open Coqast diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli index 91596ef5c..60668997b 100644 --- a/parsing/g_natsyntax.mli +++ b/parsing/g_natsyntax.mli @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* None -(***********************************************************************) +(************************************************************************) (* Declaring interpreters and uninterpreters for positive *) -(***********************************************************************) +(************************************************************************) let _ = Symbols.declare_numeral_interpreter "positive_scope" (glob_positive,positive_module) @@ -284,7 +284,7 @@ let uninterp_n p = try Some (bignat_of_n p) with Non_closed_number -> None -(***********************************************************************) +(************************************************************************) (* Declaring interpreters and uninterpreters for N *) let _ = Symbols.declare_numeral_interpreter "N_scope" @@ -348,7 +348,7 @@ let uninterp_z p = Some (bigint_of_z p) with Non_closed_number -> None -(***********************************************************************) +(************************************************************************) (* Declaring interpreters and uninterpreters for Z *) let _ = Symbols.declare_numeral_interpreter "Z_scope" @@ -360,7 +360,7 @@ let _ = Symbols.declare_numeral_interpreter "Z_scope" uninterp_z, None) -(***********************************************************************) +(************************************************************************) (* Old V7 ast Printers *) open Esyntax diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli index a8370f630..b7e6e994e 100644 --- a/parsing/g_zsyntax.mli +++ b/parsing/g_zsyntax.mli @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* env -> cbv_infos val cbv_norm : cbv_infos -> constr -> constr -(***********************************************************************) +(************************************************************************) (*i This is for cbv debug *) type cbv_value = | VAL of int * constr diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 536e292fc..c4e88f5ae 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Dyn.t), diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 9104c424a..3d88422eb 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* list0 -> list0. Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v index 0a4b51506..4accbf344 100644 --- a/test-suite/bench/lists_100.v +++ b/test-suite/bench/lists_100.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* list0 -> list0. Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 8af5c310a..fb9a27bb0 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* nat) -> t. diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index d46147843..8f3aedace 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,9 +1,9 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* nat->Prop. diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 434ec5464..f826df9a4 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* T. diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index c26cb16f9..374029bba 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (T U). End S. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 6ab77e008..9ae498d2d 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ? | (S p) => ? end. (* cannot be executed *) Abort. -(***********************************************************************) +(************************************************************************) Lemma T : nat. @@ -46,7 +46,7 @@ Refine (S ?). Abort. -(***********************************************************************) +(************************************************************************) Lemma essai2 : (x:nat)x=x. @@ -79,7 +79,7 @@ Refine Fix f{f/1 : (x:nat)x=x := Abort. -(***********************************************************************) +(************************************************************************) Lemma essai : nat. @@ -94,7 +94,7 @@ Refine (f ? O). Abort. -(***********************************************************************) +(************************************************************************) Parameter P : nat -> Prop. @@ -115,7 +115,7 @@ Refine (exist nat [x:nat](x=(S O)) (S O) ?). Abort. -(***********************************************************************) +(************************************************************************) Lemma essai : (n:nat){ x:nat | x=(S n) }. diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index dbbb3403e..3f1292765 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*