From 187dc15532f0c6f380d7bcb07adc2180c29fedc2 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 15 Mar 2001 13:38:59 +0000 Subject: entetes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 10 +++++++++- Makefile.dep | 7 +++++++ config/coq_config.mli | 7 +++++++ contrib/extraction/Extraction.v | 7 +++++++ contrib/extraction/close_env.ml | 7 +++++++ contrib/extraction/close_env.mli | 7 +++++++ contrib/extraction/extraction.ml | 7 +++++++ contrib/extraction/extraction.mli | 7 +++++++ contrib/extraction/genpp.ml | 7 +++++++ contrib/extraction/genpp.mli | 7 +++++++ contrib/extraction/miniml.mli | 7 +++++++ contrib/extraction/mlimport.ml | 7 +++++++ contrib/extraction/mlimport.mli | 7 +++++++ contrib/extraction/ocaml.ml | 7 +++++++ contrib/extraction/ocaml.mli | 7 +++++++ contrib/extraction/test_extraction.v | 7 +++++++ contrib/omega/Omega.v | 7 +++++++ contrib/omega/OmegaSyntax.v | 7 +++++++ contrib/omega/Zcomplements.v | 7 +++++++ contrib/omega/Zlogarithm.v | 7 +++++++ contrib/omega/Zpower.v | 7 +++++++ contrib/omega/coq_omega.ml | 7 +++++++ contrib/omega/omega.ml | 7 +++++++ contrib/ring/ArithRing.v | 7 +++++++ contrib/ring/Quote.v | 7 +++++++ contrib/ring/Ring.v | 7 +++++++ contrib/ring/Ring_abstract.v | 7 +++++++ contrib/ring/Ring_normalize.v | 7 +++++++ contrib/ring/Ring_theory.v | 7 +++++++ contrib/ring/ZArithRing.v | 7 +++++++ contrib/ring/quote.ml | 7 +++++++ contrib/ring/ring.ml | 7 +++++++ contrib/xml/Xml.v | 7 +++++++ contrib/xml/xml.ml | 7 +++++++ contrib/xml/xml.mli | 7 +++++++ contrib/xml/xmlcommand.ml | 7 +++++++ contrib/xml/xmlcommand.mli | 7 +++++++ contrib/xml/xmlentries.ml | 7 +++++++ dev/db_printers.ml | 7 +++++++ dev/top_printers.ml | 7 +++++++ kernel/closure.ml | 7 +++++++ kernel/closure.mli | 7 +++++++ kernel/cooking.ml | 7 +++++++ kernel/cooking.mli | 7 +++++++ kernel/declarations.ml | 7 +++++++ kernel/declarations.mli | 7 +++++++ kernel/environ.ml | 7 +++++++ kernel/environ.mli | 7 +++++++ kernel/esubst.ml | 7 +++++++ kernel/esubst.mli | 7 +++++++ kernel/evd.ml | 7 +++++++ kernel/evd.mli | 7 +++++++ kernel/indtypes.ml | 7 +++++++ kernel/indtypes.mli | 7 +++++++ kernel/inductive.ml | 7 +++++++ kernel/inductive.mli | 7 +++++++ kernel/instantiate.ml | 7 +++++++ kernel/instantiate.mli | 7 +++++++ kernel/names.ml | 7 +++++++ kernel/names.mli | 7 +++++++ kernel/reduction.ml | 7 +++++++ kernel/reduction.mli | 7 +++++++ kernel/safe_typing.ml | 7 +++++++ kernel/safe_typing.mli | 7 +++++++ kernel/sign.ml | 7 +++++++ kernel/sign.mli | 7 +++++++ kernel/term.ml | 7 +++++++ kernel/term.mli | 7 +++++++ kernel/type_errors.ml | 7 +++++++ kernel/type_errors.mli | 7 +++++++ kernel/typeops.ml | 7 +++++++ kernel/typeops.mli | 7 +++++++ kernel/univ.ml | 7 +++++++ kernel/univ.mli | 7 +++++++ lib/bij.ml | 7 +++++++ lib/bij.mli | 7 +++++++ lib/bstack.ml | 7 +++++++ lib/bstack.mli | 7 +++++++ lib/dyn.ml | 7 +++++++ lib/dyn.mli | 7 +++++++ lib/edit.ml | 7 +++++++ lib/edit.mli | 7 +++++++ lib/explore.ml | 7 +++++++ lib/explore.mli | 7 +++++++ lib/gmap.ml | 7 +++++++ lib/gmap.mli | 7 +++++++ lib/gmapl.ml | 7 +++++++ lib/gmapl.mli | 7 +++++++ lib/gset.ml | 7 +++++++ lib/gset.mli | 7 +++++++ lib/hashcons.ml | 7 +++++++ lib/hashcons.mli | 7 +++++++ lib/options.ml | 7 +++++++ lib/options.mli | 7 +++++++ lib/pp.ml | 7 +++++++ lib/pp.mli | 7 +++++++ lib/pp_control.ml | 7 +++++++ lib/pp_control.mli | 7 +++++++ lib/profile.ml | 7 +++++++ lib/profile.mli | 7 +++++++ lib/stamps.ml | 7 +++++++ lib/stamps.mli | 7 +++++++ lib/system.ml | 7 +++++++ lib/system.mli | 7 +++++++ lib/tlm.ml | 7 +++++++ lib/tlm.mli | 7 +++++++ lib/util.ml | 7 +++++++ lib/util.mli | 7 +++++++ library/declare.ml | 7 +++++++ library/declare.mli | 7 +++++++ library/global.ml | 7 +++++++ library/global.mli | 7 +++++++ library/goptions.ml | 7 +++++++ library/goptions.mli | 7 +++++++ library/impargs.ml | 7 +++++++ library/impargs.mli | 7 +++++++ library/indrec.ml | 7 +++++++ library/indrec.mli | 7 +++++++ library/lib.ml | 7 +++++++ library/lib.mli | 7 +++++++ library/libobject.ml | 7 +++++++ library/libobject.mli | 7 +++++++ library/library.ml | 7 +++++++ library/library.mli | 7 +++++++ library/nametab.ml | 7 +++++++ library/nametab.mli | 7 +++++++ library/states.ml | 7 +++++++ library/states.mli | 7 +++++++ library/summary.ml | 7 +++++++ library/summary.mli | 7 +++++++ parsing/ast.ml | 7 +++++++ parsing/ast.mli | 7 +++++++ parsing/astterm.ml | 7 +++++++ parsing/astterm.mli | 7 +++++++ parsing/coqast.ml | 7 +++++++ parsing/coqast.mli | 7 +++++++ parsing/coqlib.ml | 7 +++++++ parsing/coqlib.mli | 7 +++++++ parsing/egrammar.ml | 7 +++++++ parsing/egrammar.mli | 7 +++++++ parsing/esyntax.ml | 7 +++++++ parsing/esyntax.mli | 7 +++++++ parsing/extend.ml4 | 7 +++++++ parsing/extend.mli | 7 +++++++ parsing/g_basevernac.ml4 | 7 +++++++ parsing/g_cases.ml4 | 7 +++++++ parsing/g_constr.ml4 | 7 +++++++ parsing/g_minicoq.ml4 | 7 +++++++ parsing/g_minicoq.mli | 7 +++++++ parsing/g_natsyntax.ml | 7 +++++++ parsing/g_natsyntax.mli | 7 +++++++ parsing/g_prim.ml4 | 7 +++++++ parsing/g_proofs.ml4 | 7 +++++++ parsing/g_rsyntax.ml | 7 +++++++ parsing/g_tactic.ml4 | 7 +++++++ parsing/g_vernac.ml4 | 7 +++++++ parsing/g_zsyntax.ml | 7 +++++++ parsing/g_zsyntax.mli | 7 +++++++ parsing/lexer.ml4 | 7 +++++++ parsing/lexer.mli | 7 +++++++ parsing/pcoq.ml4 | 7 +++++++ parsing/pcoq.mli | 7 +++++++ parsing/pretty.ml | 7 +++++++ parsing/pretty.mli | 7 +++++++ parsing/printer.ml | 7 +++++++ parsing/printer.mli | 7 +++++++ parsing/q_coqast.ml4 | 7 +++++++ parsing/search.ml | 7 +++++++ parsing/search.mli | 7 +++++++ parsing/termast.ml | 7 +++++++ parsing/termast.mli | 7 +++++++ pretyping/cases.ml | 7 +++++++ pretyping/cases.mli | 7 +++++++ pretyping/cbv.ml | 7 +++++++ pretyping/cbv.mli | 7 +++++++ pretyping/classops.ml | 7 +++++++ pretyping/classops.mli | 7 +++++++ pretyping/coercion.ml | 7 +++++++ pretyping/coercion.mli | 7 +++++++ pretyping/detyping.ml | 7 +++++++ pretyping/detyping.mli | 7 +++++++ pretyping/evarconv.ml | 7 +++++++ pretyping/evarconv.mli | 7 +++++++ pretyping/evarutil.ml | 7 +++++++ pretyping/evarutil.mli | 7 +++++++ pretyping/multcase.mli | 7 +++++++ pretyping/pattern.ml | 7 +++++++ pretyping/pattern.mli | 7 +++++++ pretyping/pretype_errors.ml | 7 +++++++ pretyping/pretype_errors.mli | 7 +++++++ pretyping/pretyping.ml | 7 +++++++ pretyping/pretyping.mli | 7 +++++++ pretyping/rawterm.ml | 7 +++++++ pretyping/rawterm.mli | 7 +++++++ pretyping/recordops.ml | 7 +++++++ pretyping/recordops.mli | 7 +++++++ pretyping/retyping.ml | 7 +++++++ pretyping/retyping.mli | 7 +++++++ pretyping/syntax_def.ml | 7 +++++++ pretyping/syntax_def.mli | 7 +++++++ pretyping/tacred.ml | 7 +++++++ pretyping/tacred.mli | 7 +++++++ pretyping/typing.ml | 7 +++++++ pretyping/typing.mli | 7 +++++++ proofs/clenv.ml | 7 +++++++ proofs/clenv.mli | 7 +++++++ proofs/evar_refiner.ml | 7 +++++++ proofs/evar_refiner.mli | 7 +++++++ proofs/logic.ml | 7 +++++++ proofs/logic.mli | 7 +++++++ proofs/pfedit.ml | 7 +++++++ proofs/pfedit.mli | 7 +++++++ proofs/proof_trees.ml | 7 +++++++ proofs/proof_trees.mli | 7 +++++++ proofs/proof_type.ml | 7 +++++++ proofs/proof_type.mli | 7 +++++++ proofs/refiner.ml | 7 +++++++ proofs/refiner.mli | 7 +++++++ proofs/tacinterp.ml | 7 +++++++ proofs/tacinterp.mli | 7 +++++++ proofs/tacmach.ml | 7 +++++++ proofs/tacmach.mli | 7 +++++++ proofs/tactic_debug.ml | 7 +++++++ proofs/tactic_debug.mli | 7 +++++++ scripts/coqc.ml | 7 +++++++ scripts/coqmktop.ml | 7 +++++++ states/MakeInitial.v | 7 +++++++ syntax/MakeBare.v | 7 +++++++ syntax/PPCases.v | 7 +++++++ syntax/PPConstr.v | 7 +++++++ syntax/PPTactic.v | 7 +++++++ tactics/AutoRewrite.v | 7 +++++++ tactics/EAuto.v | 7 +++++++ tactics/EqDecide.v | 7 +++++++ tactics/Equality.v | 7 +++++++ tactics/Inv.v | 7 +++++++ tactics/Refine.v | 7 +++++++ tactics/Tauto.v | 7 +++++++ tactics/auto.ml | 7 +++++++ tactics/auto.mli | 7 +++++++ tactics/autorewrite.ml | 7 +++++++ tactics/autorewrite.mli | 7 +++++++ tactics/btermdn.ml | 7 +++++++ tactics/btermdn.mli | 7 +++++++ tactics/dhyp.ml | 7 +++++++ tactics/dhyp.mli | 7 +++++++ tactics/dn.ml | 7 +++++++ tactics/dn.mli | 7 +++++++ tactics/eauto.ml | 7 +++++++ tactics/elim.ml | 7 +++++++ tactics/elim.mli | 7 +++++++ tactics/eqdecide.ml | 7 +++++++ tactics/equality.ml | 7 +++++++ tactics/equality.mli | 7 +++++++ tactics/hiddentac.ml | 7 +++++++ tactics/hiddentac.mli | 7 +++++++ tactics/hipattern.ml | 7 +++++++ tactics/hipattern.mli | 7 +++++++ tactics/inv.ml | 7 +++++++ tactics/inv.mli | 7 +++++++ tactics/leminv.ml | 7 +++++++ tactics/nbtermdn.ml | 7 +++++++ tactics/nbtermdn.mli | 7 +++++++ tactics/refine.ml | 7 +++++++ tactics/refine.mli | 7 +++++++ tactics/tacentries.ml | 7 +++++++ tactics/tacentries.mli | 7 +++++++ tactics/tacticals.ml | 7 +++++++ tactics/tacticals.mli | 7 +++++++ tactics/tactics.ml | 7 +++++++ tactics/tactics.mli | 7 +++++++ tactics/tauto.ml4 | 7 +++++++ tactics/termdn.ml | 7 +++++++ tactics/termdn.mli | 7 +++++++ tactics/wcclausenv.ml | 7 +++++++ tactics/wcclausenv.mli | 7 +++++++ test-suite/bench/lists-100.v | 7 +++++++ test-suite/bench/lists_100.v | 7 +++++++ test-suite/failure/Tauto.v | 7 +++++++ test-suite/failure/clash_cons.v | 7 +++++++ test-suite/failure/fixpoint1.v | 7 +++++++ test-suite/failure/illtype1.v | 7 +++++++ test-suite/failure/positivity.v | 7 +++++++ test-suite/failure/redef.v | 7 +++++++ test-suite/failure/search.v | 7 +++++++ test-suite/success/Apply.v | 7 +++++++ test-suite/success/Cases.v | 7 +++++++ test-suite/success/Check.v | 7 +++++++ test-suite/success/Tauto.v | 7 +++++++ test-suite/success/eauto.v | 7 +++++++ test-suite/success/eqdecide.v | 7 +++++++ test-suite/success/evars.v | 7 +++++++ test-suite/success/fix.v | 7 +++++++ test-suite/success/inds_type_sec.v | 7 +++++++ test-suite/success/induct.v | 7 +++++++ test-suite/success/mutual_ind.v | 7 +++++++ test-suite/success/unfold.v | 7 +++++++ test-suite/tactics/TestRefine.v | 7 +++++++ theories/Arith/Arith.v | 7 +++++++ theories/Arith/Between.v | 7 +++++++ theories/Arith/Compare.v | 7 +++++++ theories/Arith/Compare_dec.v | 7 +++++++ theories/Arith/Div.v | 7 +++++++ theories/Arith/Div2.v | 7 +++++++ theories/Arith/EqNat.v | 7 +++++++ theories/Arith/Euclid_def.v | 7 +++++++ theories/Arith/Euclid_proof.v | 7 +++++++ theories/Arith/Even.v | 7 +++++++ theories/Arith/Gt.v | 7 +++++++ theories/Arith/Le.v | 7 +++++++ theories/Arith/Lt.v | 7 +++++++ theories/Arith/Min.v | 7 +++++++ theories/Arith/Minus.v | 7 +++++++ theories/Arith/Mult.v | 7 +++++++ theories/Arith/Peano_dec.v | 7 +++++++ theories/Arith/Plus.v | 7 +++++++ theories/Arith/Wf_nat.v | 7 +++++++ theories/Bool/Bool.v | 7 +++++++ theories/Bool/DecBool.v | 7 +++++++ theories/Bool/IfProp.v | 7 +++++++ theories/Bool/Sumbool.v | 7 +++++++ theories/Bool/Zerob.v | 7 +++++++ theories/Init/Datatypes.v | 7 +++++++ theories/Init/DatatypesSyntax.v | 7 +++++++ theories/Init/Logic.v | 7 +++++++ theories/Init/LogicSyntax.v | 7 +++++++ theories/Init/Logic_Type.v | 7 +++++++ theories/Init/Logic_TypeSyntax.v | 7 +++++++ theories/Init/Peano.v | 7 +++++++ theories/Init/Prelude.v | 7 +++++++ theories/Init/Specif.v | 7 +++++++ theories/Init/SpecifSyntax.v | 7 +++++++ theories/Init/Wf.v | 7 +++++++ theories/Lists/List.v | 7 +++++++ theories/Lists/ListSet.v | 7 +++++++ theories/Lists/PolyList.v | 7 +++++++ theories/Lists/PolyListSyntax.v | 7 +++++++ theories/Lists/Streams.v | 7 +++++++ theories/Lists/TheoryList.v | 7 +++++++ theories/Logic/Classical.v | 7 +++++++ theories/Logic/Classical_Pred_Set.v | 7 +++++++ theories/Logic/Classical_Pred_Type.v | 7 +++++++ theories/Logic/Classical_Prop.v | 7 +++++++ theories/Logic/Classical_Type.v | 7 +++++++ theories/Logic/Eqdep.v | 7 +++++++ theories/Logic/Eqdep_dec.v | 7 +++++++ theories/Num/AddProps.v | 7 +++++++ theories/Num/Axioms.v | 7 +++++++ theories/Num/Definitions.v | 7 +++++++ theories/Num/DiscrAxioms.v | 7 +++++++ theories/Num/DiscrProps.v | 7 +++++++ theories/Num/GeAxioms.v | 7 +++++++ theories/Num/GeProps.v | 7 +++++++ theories/Num/GtAxioms.v | 7 +++++++ theories/Num/GtProps.v | 7 +++++++ theories/Num/LeAxioms.v | 7 +++++++ theories/Num/LeProps.v | 7 +++++++ theories/Num/LtProps.v | 7 +++++++ theories/Num/NSyntax.v | 7 +++++++ theories/Num/OppAxioms.v | 7 +++++++ theories/Num/OppProps.v | 7 +++++++ theories/Num/SubProps.v | 7 +++++++ theories/Reals/R_Ifp.v | 7 +++++++ theories/Reals/Raxioms.v | 7 +++++++ theories/Reals/Rbase.v | 7 +++++++ theories/Reals/Rbasic_fun.v | 7 +++++++ theories/Reals/Rdefinitions.v | 7 +++++++ theories/Reals/Rderiv.v | 7 +++++++ theories/Reals/Reals.v | 7 +++++++ theories/Reals/Rfunctions.v | 7 +++++++ theories/Reals/Rlimit.v | 7 +++++++ theories/Reals/Rsyntax.v | 7 +++++++ theories/Reals/TypeSyntax.v | 7 +++++++ theories/Relations/Newman.v | 7 +++++++ theories/Relations/Operators_Properties.v | 7 +++++++ theories/Relations/Relation_Definitions.v | 7 +++++++ theories/Relations/Relation_Operators.v | 7 +++++++ theories/Relations/Relations.v | 7 +++++++ theories/Relations/Rstar.v | 7 +++++++ theories/Sets/Classical_sets.v | 7 +++++++ theories/Sets/Constructive_sets.v | 7 +++++++ theories/Sets/Cpo.v | 7 +++++++ theories/Sets/Ensembles.v | 7 +++++++ theories/Sets/Finite_sets.v | 7 +++++++ theories/Sets/Finite_sets_facts.v | 7 +++++++ theories/Sets/Image.v | 7 +++++++ theories/Sets/Infinite_sets.v | 7 +++++++ theories/Sets/Integers.v | 7 +++++++ theories/Sets/Multiset.v | 7 +++++++ theories/Sets/Partial_Order.v | 7 +++++++ theories/Sets/Permut.v | 7 +++++++ theories/Sets/Powerset.v | 7 +++++++ theories/Sets/Powerset_Classical_facts.v | 7 +++++++ theories/Sets/Powerset_facts.v | 7 +++++++ theories/Sets/Relations_1.v | 7 +++++++ theories/Sets/Relations_1_facts.v | 7 +++++++ theories/Sets/Relations_2.v | 7 +++++++ theories/Sets/Relations_2_facts.v | 7 +++++++ theories/Sets/Relations_3.v | 7 +++++++ theories/Sets/Relations_3_facts.v | 7 +++++++ theories/Sets/Uniset.v | 7 +++++++ theories/Wellfounded/Disjoint_Union.v | 7 +++++++ theories/Wellfounded/Inclusion.v | 7 +++++++ theories/Wellfounded/Inverse_Image.v | 7 +++++++ theories/Wellfounded/Lexicographic_Exponentiation.v | 7 +++++++ theories/Wellfounded/Lexicographic_Product.v | 7 +++++++ theories/Wellfounded/Transitive_Closure.v | 7 +++++++ theories/Wellfounded/Union.v | 7 +++++++ theories/Wellfounded/Well_Ordering.v | 7 +++++++ theories/Wellfounded/Wellfounded.v | 7 +++++++ theories/Zarith/Wf_Z.v | 7 +++++++ theories/Zarith/ZArith.v | 7 +++++++ theories/Zarith/ZArith_dec.v | 7 +++++++ theories/Zarith/Zmisc.v | 7 +++++++ theories/Zarith/Zsyntax.v | 7 +++++++ theories/Zarith/auxiliary.v | 7 +++++++ theories/Zarith/fast_integer.v | 7 +++++++ theories/Zarith/zarith_aux.v | 7 +++++++ tools/coq-tex.ml | 7 +++++++ tools/coq_makefile.ml | 7 +++++++ tools/coqdep.ml | 7 +++++++ tools/coqdep_lexer.mll | 7 +++++++ tools/gallina.ml | 7 +++++++ tools/gallina_lexer.mll | 7 +++++++ toplevel/class.ml | 7 +++++++ toplevel/class.mli | 7 +++++++ toplevel/command.ml | 7 +++++++ toplevel/command.mli | 7 +++++++ toplevel/coqinit.ml | 7 +++++++ toplevel/coqinit.mli | 7 +++++++ toplevel/coqtop.ml | 7 +++++++ toplevel/coqtop.mli | 7 +++++++ toplevel/discharge.ml | 7 +++++++ toplevel/discharge.mli | 7 +++++++ toplevel/errors.ml | 7 +++++++ toplevel/errors.mli | 7 +++++++ toplevel/fhimsg.ml | 7 +++++++ toplevel/fhimsg.mli | 7 +++++++ toplevel/himsg.ml | 7 +++++++ toplevel/himsg.mli | 7 +++++++ toplevel/line_oriented_parser.ml | 7 +++++++ toplevel/line_oriented_parser.mli | 7 +++++++ toplevel/metasyntax.ml | 7 +++++++ toplevel/metasyntax.mli | 7 +++++++ toplevel/minicoq.ml | 7 +++++++ toplevel/mltop.ml4 | 7 +++++++ toplevel/mltop.mli | 7 +++++++ toplevel/protectedtoplevel.ml | 7 +++++++ toplevel/protectedtoplevel.mli | 7 +++++++ toplevel/record.ml | 7 +++++++ toplevel/record.mli | 7 +++++++ toplevel/recordobj.ml | 7 +++++++ toplevel/recordobj.mli | 7 +++++++ toplevel/searchisos.mli | 7 +++++++ toplevel/toplevel.ml | 7 +++++++ toplevel/toplevel.mli | 7 +++++++ toplevel/usage.ml | 7 +++++++ toplevel/usage.mli | 7 +++++++ toplevel/vernac.ml | 7 +++++++ toplevel/vernac.mli | 7 +++++++ toplevel/vernacentries.ml | 7 +++++++ toplevel/vernacentries.mli | 7 +++++++ toplevel/vernacinterp.ml | 7 +++++++ toplevel/vernacinterp.mli | 7 +++++++ 464 files changed, 3250 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b6fbb62bff..4c9b546b6a 100644 --- a/Makefile +++ b/Makefile @@ -1,5 +1,13 @@ +####################################################################### +# 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 62a34dbd41..0a4b515066 100644 --- a/test-suite/bench/lists_100.v +++ b/test-suite/bench/lists_100.v @@ -1,3 +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 3e8bbeeb17..8af5c310a2 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,3 +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 0c821906e0..d461478430 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,2 +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 f118bc830c..434ec5464e 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* T. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 188ce73d54..6d52ec4c64 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Set. Variable cons:(T:Set) T -> (list T) -> (list T). diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index 3834fc0f52..c26cb16f92 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -1,3 +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 cffc8ba7af..6ab77e0088 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(*