Modification de la table des tactic Definitions pour eviter l'ecriture

de fonctions dans les .vo
ajout de lemmes dans EqNat, Logic_Type
suppression de PolyListSyntax qui redefinissait le Infix de append
Recherche d'instances a reecrire dans les Cases et les FixPoint


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@820 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 137 insertions, 63 deletions

diff --git a/.depend.coq b/.depend.coq
index 5dbe990ce6..d7d01a3a8e 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -1,83 +1,85 @@
+theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
+theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
+theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
 theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo
 theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo
-theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
 theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
-theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo
+theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo
 theories/Zarith/Wf_Z.vo: theories/Zarith/Wf_Z.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo
-theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
-theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo
 theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo
-theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
 theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo
-theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
+theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo
 theories/Sets/Relations_2_facts.vo: theories/Sets/Relations_2_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo
-theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
+theories/Sets/Relations_2.vo: theories/Sets/Relations_2.v theories/Sets/Relations_1.vo
 theories/Sets/Relations_1_facts.vo: theories/Sets/Relations_1_facts.v theories/Sets/Relations_1.vo
-theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
+theories/Sets/Relations_1.vo: theories/Sets/Relations_1.v
 theories/Sets/Powerset_facts.vo: theories/Sets/Powerset_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo
 theories/Sets/Powerset_Classical_facts.vo: theories/Sets/Powerset_Classical_facts.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo
+theories/Sets/Powerset.vo: theories/Sets/Powerset.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
 theories/Sets/Permut.vo: theories/Sets/Permut.v
 theories/Sets/Partial_Order.vo: theories/Sets/Partial_Order.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo
 theories/Sets/Multiset.vo: theories/Sets/Multiset.v theories/Sets/Permut.vo theories/Arith/Plus.vo
 theories/Sets/Integers.vo: theories/Sets/Integers.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo theories/Sets/Infinite_sets.vo theories/Arith/Compare_dec.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo theories/Sets/Cpo.vo
 theories/Sets/Infinite_sets.vo: theories/Sets/Infinite_sets.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo
 theories/Sets/Image.vo: theories/Sets/Image.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo theories/Arith/Le.vo theories/Sets/Finite_sets_facts.vo
-theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo
 theories/Sets/Finite_sets_facts.vo: theories/Sets/Finite_sets_facts.v theories/Sets/Finite_sets.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo theories/Sets/Classical_sets.vo theories/Sets/Powerset.vo theories/Sets/Powerset_facts.vo theories/Sets/Powerset_Classical_facts.vo theories/Arith/Gt.vo theories/Arith/Lt.vo
+theories/Sets/Finite_sets.vo: theories/Sets/Finite_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo
 theories/Sets/Ensembles.vo: theories/Sets/Ensembles.v
 theories/Sets/Cpo.vo: theories/Sets/Cpo.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo theories/Sets/Partial_Order.vo
 theories/Sets/Constructive_sets.vo: theories/Sets/Constructive_sets.v theories/Sets/Ensembles.vo
 theories/Sets/Classical_sets.vo: theories/Sets/Classical_sets.v theories/Sets/Ensembles.vo theories/Sets/Constructive_sets.vo theories/Logic/Classical_Type.vo
 theories/Relations/Rstar.vo: theories/Relations/Rstar.v
 theories/Relations/Relations.vo: theories/Relations/Relations.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Operators_Properties.vo
-theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v theories/Relations/Relation_Definitions.vo theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo
+theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators.v theories/Relations/Relation_Definitions.vo theories/Lists/PolyList.vo
 theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definitions.v
 theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
 theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo
 theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
 theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
 theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo
 theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo
 theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
 theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo theories/Logic/Classical_Prop.vo contrib/omega/Omega.vo
 theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/Zarith/ZArith.vo theories/Reals/TypeSyntax.vo
-theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
+theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
 theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v
-theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
+theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v
 theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
 theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v
 theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
 theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo
+theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo
 theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo
 theories/Lists/Streams.vo: theories/Lists/Streams.v
-theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
+theories/Lists/Program.vo: theories/Lists/Program.v tactics/Refine.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
-theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
+theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
+theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
 theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
-theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo
+theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo
 theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo
-theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
-theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo
+theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo
 theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo
-theories/Init/Datatypes.vo: theories/Init/Datatypes.v
+theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo
 theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo
+theories/Init/Datatypes.vo: theories/Init/Datatypes.v
 theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo
 theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
 theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo
 theories/Bool/DecBool.vo: theories/Bool/DecBool.v
+theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo
 theories/Bool/Bool.vo: theories/Bool/Bool.v
 theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
 theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v
 theories/Arith/Mult.vo: theories/Arith/Mult.v theories/Arith/Plus.vo theories/Arith/Minus.vo
-theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
 theories/Arith/Minus.vo: theories/Arith/Minus.v theories/Arith/Lt.vo theories/Arith/Le.vo
+theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
 theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
 theories/Arith/Le.vo: theories/Arith/Le.v
 theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
@@ -85,28 +87,28 @@ theories/Arith/Even.vo: theories/Arith/Even.v
 theories/Arith/Euclid_proof.vo: theories/Arith/Euclid_proof.v theories/Arith/Minus.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
 theories/Arith/Euclid_def.vo: theories/Arith/Euclid_def.v theories/Arith/Mult.vo
 theories/Arith/EqNat.vo: theories/Arith/EqNat.v
-theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo
 theories/Arith/Div2.vo: theories/Arith/Div2.v theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Compare_dec.vo theories/Arith/Even.vo
-theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
+theories/Arith/Div.vo: theories/Arith/Div.v theories/Arith/Le.vo theories/Arith/Euclid_def.vo theories/Arith/Compare_dec.vo
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo
+theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo
 test-suite/tactics/TestRefine.vo: test-suite/tactics/TestRefine.v tactics/Refine.vo theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Arith/Lt.vo
-test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
 test-suite/bench/lists_100.vo: test-suite/bench/lists_100.v
+test-suite/bench/lists-100.vo: test-suite/bench/lists-100.v
 contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo
 contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo
-contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/ring.cmo
 contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo
 contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo
 contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo
+contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/ring.cmo
 contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/quote.cmo
 contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo
 contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo
 contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo
 contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo
-contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
 contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v
+contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo
 tactics/Tauto.vo: tactics/Tauto.v
 tactics/Refine.vo: tactics/Refine.v
 tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo
diff --git a/Makefile b/Makefile
index de15e784f4..202eb78be2 100644
--- a/Makefile
+++ b/Makefile
@@ -257,7 +257,7 @@ ZARITHVO=theories/Zarith/Wf_Z.vo        theories/Zarith/Zsyntax.vo \
 	 theories/Zarith/ZArith_dec.vo  theories/Zarith/fast_integer.vo \
 	 theories/Zarith/Zmisc.vo       theories/Zarith/zarith_aux.vo
 
-LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
+LISTSVO=theories/Lists/List.vo      \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo        \
         theories/Lists/PolyList.vo  theories/Lists/TheoryList.vo
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 97fe3c7dc0..5c9e5894ea 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -20,9 +20,6 @@ val mk_Prop : sorts
 
 val print_sort : sorts -> std_ppcmds
 
-(*s The operators of the Calculus of Inductive Constructions. 
-  ['a] is the type of sorts. ([XTRA] is an extra slot, for putting in 
-  whatever sort of operator we need for whatever sort of application.) *)
 
 type existential_key = int
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 962073127d..f78ab96113 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -667,6 +667,12 @@ let clenv_refine_cast kONT clenv gls =
    try to find a subterm of cl which matches op, if op is just a Meta
    FAIL because we cannot find a binding *)
 
+let iter_fail f a = let n = Array.length a in 
+		    let rec ffail i = if i = n then error "iter_fail" 
+                    else try f a.(i) 
+		    with ex when catchable_exception ex -> ffail (i+1)
+		    in ffail 0
+
 let constrain_clenv_to_subterm clause (op,cl) =
   let rec matchrec cl =
     let cl = strip_outer_cast cl in
@@ -676,8 +682,11 @@ let constrain_clenv_to_subterm clause (op,cl) =
        else error "Bound 1"
      with ex when catchable_exception ex ->
        (match kind_of_term cl with 
-	  | IsApp (f,args) ->
-	      let n = Array.length args in
+	  | IsApp (f,args) ->  (try 
+		 matchrec f
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec args)
+	(* let n = Array.length args in
 	      assert (n>0);
 	      let c1 = mkApp (f,Array.sub args 0 (n-1)) in
 	      let c2 = args.(n-1) in
@@ -685,6 +694,30 @@ let constrain_clenv_to_subterm clause (op,cl) =
 		 matchrec c1
 	       with ex when catchable_exception ex -> 
 		 matchrec c2)
+	   *)
+          | IsMutCase(_,_,c,lf) -> (* does not search in the predicate *)
+	       (try 
+		 matchrec c
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec lf)
+	  | IsLetIn(_,c1,_,c2) -> 
+	       (try 
+		 matchrec c1
+	       with ex when catchable_exception ex -> 
+		 matchrec c2)
+
+	  | IsFix(_,(types,_,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec terms)
+	
+	  | IsCoFix(_,(types,_,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec terms)
+
           | IsProd (_,t,c) ->
 	      (try 
 		 matchrec t 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 09dc5a0955..22905459f5 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -156,25 +156,6 @@ let _ =
       Summary.unfreeze_function = unfreeze;
       Summary.init_function     = init }
 
-let (inMD,outMD) =
-  let add (na,td) = mactab := Gmap.add na td !mactab in
-  let cache_md (_,(na,td)) = add (na,td) in 
-    declare_object ("TACTIC-DEFINITION",
-       {cache_function         = cache_md;
-        load_function          = (fun _ -> ());
-        open_function          = (fun _ -> ());
-        specification_function = (fun x -> x)})
-
-(* Adds a Tactic Definition in the table *)
-let add_tacdef na vbody =
-  begin
-    if Gmap.mem na !mactab then
-      errorlabstrm "Tacdef.add_tacdef" 
-        [<'sTR "There is already a Tactic Definition named "; 'sTR na>];
-    let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
-    if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >]
-  end
-
 (* Unboxes the tactic_arg *)
 let unvarg = function
   | VArg a -> a
@@ -956,3 +937,25 @@ let vernac_interp_atomic =
 let bad_tactic_args s =
   anomalylabstrm s
     [<'sTR "Tactic "; 'sTR s; 'sTR " called with bad arguments">]
+
+let (inMD,outMD) =
+  let add (na,td) = mactab := Gmap.add na td !mactab in
+  let cache_md (_,(na,td)) =  
+    let ve=val_interp (Evd.empty,Environ.empty_env,[],[],None,get_debug ()) td 
+    in add (na,ve) in 
+    declare_object ("TACTIC-DEFINITION",
+       {cache_function         = cache_md;
+        load_function          = cache_md;
+        open_function          = (fun _ -> ());
+        specification_function = (fun x -> x)})
+
+(* Adds a Tactic Definition in the table *)
+let add_tacdef na vbody =
+  begin
+    if Gmap.mem na !mactab then
+      errorlabstrm "Tacdef.add_tacdef" 
+        [<'sTR "There is already a Tactic Definition named "; 'sTR na>];
+    let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
+    if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >]
+  end
+
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index ee5d67966a..d0ec28ea05 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -49,7 +49,7 @@ val set_debug : debug_info -> unit
 val get_debug : unit -> debug_info
 
 (* Adds a Tactic Definition in the table *)
-val add_tacdef : string -> value -> unit
+val add_tacdef : string -> Coqast.t -> unit
 
 (* Interprets any expression *)
 val val_interp : interp_sign -> Coqast.t -> value
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index dde9daa4c3..ecce3f840a 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -51,3 +51,18 @@ Fixpoint  beq_nat [n:nat] : nat -> bool :=
              | (S _)   O     => false
              | (S n1) (S m1) => (beq_nat n1 m1)
           end.
+
+Lemma beq_nat_refl : (x:nat)true=(beq_nat x x).
+Proof.
+  Induction x; Simpl; Auto.
+Qed.
+
+Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y.
+Proof.
+  Double Induction 1 2; Simpl.
+    Reflexivity.
+    Intros; Discriminate H0.
+    Intros; Discriminate H0.
+    Intros; Case (H0 ? H1); Reflexivity.
+Defined.
+
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 1cd3ad8bef..b78fcb93b4 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -165,6 +165,41 @@ Definition identityT_rect_r :
  Intros A x P H y H0; Case sym_idT with 1:= H0; Trivial.
 Defined.
 
+Inductive sigT [A:Set; P:A->Prop] : Type := existT : (x:A)(P x)->(sigT A P).
+
+Section sigT_proj.
+
+  Variable A : Set.
+  Variable P : A->Prop.
+
+  Definition projT1 := [H:(sigT A P)]
+    let (x, _) = H in x.
+  Definition projT2 := [H:(sigT A P)]<[H:(sigT A P)](P (projT1 H))>
+    let (_, h) = H in h.
+
+End sigT_proj.
+
+Inductive prodT [A,B:Type] : Type := pairT : A -> B -> (prodT A B).
+
+Section prodT_proj.
+
+  Variables A, B : Type.
+
+  Definition fstT := [H:(prodT A B)]Cases H of (pairT x _) => x end.
+  Definition sndT := [H:(prodT A B)]Cases H of (pairT _ y) => y end.
+
+End prodT_proj.
+
+Definition prodT_uncurry : (A,B,C:Type)((prodT A B)->C)->A->B->C :=
+  [A,B,C:Type; f:((prodT A B)->C); x:A; y:B]
+  (f (pairT A B x y)).
+
+Definition prodT_curry : (A,B,C:Type)(A->B->C)->(prodT A B)->C :=
+  [A,B,C:Type; f:(A->B->C); p:(prodT A B)]
+  Cases p of
+  | (pairT x y) => (f x y)
+  end.
+
 Hints Immediate sym_idT sym_not_idT : core v62.
 
 
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
deleted file mode 100644
index a19a3dcc14..0000000000
--- a/theories/Lists/PolyListSyntax.v
+++ /dev/null
@@ -1,7 +0,0 @@
-
-(* $Id$ *)
-
-(* Syntax for list concatenation *)
-Require PolyList.
-
-Infix RIGHTA 7 "^" app.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 1944b60cdb..546d97f90b 100755
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -11,7 +11,6 @@
 
 Require Relation_Definitions.
 Require PolyList.
-Require PolyListSyntax.
 
 (* Some operators to build relations *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a4c50cf755..5ae0500398 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1218,10 +1218,7 @@ let _ =
   add "TACDEF"
     (let rec tacdef_fun lacc=function
         (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl ->
-          let ve=
-            val_interp (empty,empty_env,[],[],None,get_debug ()) tacexp
-          in
-            tacdef_fun ((string_of_id name,ve)::lacc) tl
+          tacdef_fun ((string_of_id name,tacexp)::lacc) tl
        |[] ->
          fun () ->
            List.iter (fun (name,ve) -> Tacinterp.add_tacdef name ve) lacc