petits changements cosmetiques sur les tactiques

+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses
definies


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

11 files changed, 168 insertions, 289 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9911e449f9..674b090c39 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -752,10 +752,10 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	(tclTRY_sign decomp_empty_term extra_sign)
 	::
 	(List.map 
-	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
-		(tclTHEN 
-		   (clear_one id)
-		   (search_gen decomp p db_list local_db [])))
+	   (fun id -> tclTHENSEQ
+               [decomp_unary_term (mkVar id);
+                clear [id];
+		search_gen decomp p db_list local_db []])
 	   (pf_ids_of_hyps goal)) 
   in
   let intro_tac = 
@@ -881,12 +881,9 @@ let compileAutoArg contac = function
            (List.map 
               (fun (id,_,typ) -> 
                 let cl = snd (decompose_prod (body_of_type typ)) in
-                 if (Hipattern.is_conjunction cl)
+                 if Hipattern.is_conjunction cl
 		 then 
-		   (tclTHEN
-                      (tclTHEN (simplest_elim (mkVar id)) 
-                         (clear_one id))
-                      contac) 
+		   tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] 
                  else 
 		   tclFAIL 0) ctx) g)
   | UsingTDB ->  
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ce26640c0d..4008f10f7c 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -71,7 +71,7 @@ and general_decompose recognizer id =
   elimHypThen
     (introElimAssumsThen
        (fun bas ->
-	  tclTHEN (clear_one id)
+	  tclTHEN (clear [id])
 	    (tclMAP (general_decompose_on_hyp recognizer)
                (ids_of_named_context bas.assums))))
     id
@@ -86,10 +86,11 @@ let up_to_delta = ref false (* true *)
 let general_decompose recognizer c gl = 
   let typc = pf_type_of gl c in  
   (tclTHENS (cut typc) 
-     [(tclTHEN (intro_using tmphyp_name)
-         (onLastHyp
-	    (ifOnHyp recognizer (general_decompose recognizer) clear_one)));
-      (exact_no_check c)]) gl
+    [tclTHEN (intro_using tmphyp_name)
+      (onLastHyp
+	(ifOnHyp recognizer (general_decompose recognizer)
+          (fun id -> clear [id])));
+     exact_no_check c]) gl
 
 let head_in gls indl t =
   try
@@ -176,8 +177,9 @@ let induction_trailer abs_i abs_j bargs =
 	      ([],fvty) possible_bring_hyps
 	  in
           let ids = List.rev (ids_of_named_context hyps) in
-	  (tclTHEN (tclTHEN (bring_hyps hyps) (clear_clauses ids))
-             (simple_elimination (mkVar id))) gls))
+	  (tclTHENSEQ
+            [bring_hyps hyps; clear ids; simple_elimination (mkVar id)])
+          gls))
 
 let double_ind abs_i abs_j gls =
   let cl = pf_concl gls in 
@@ -200,18 +202,17 @@ let _ = add_tactic "DoubleInd" dyn_double_ind
 (*****************************)
 
 let rec intro_pattern p = 
-  let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))))
-  and case_last  = (tclLAST_HYP h_simplest_case) in  
+  let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
+  and case_last  = tclLAST_HYP h_simplest_case in  
   match p with
-    | WildPat    -> (tclTHEN intro clear_last)
+    | WildPat    -> tclTHEN intro clear_last
     | IdPat  id  -> intro_mustbe_force id
-    | DisjPat l  -> (tclTHEN introf
+    | DisjPat l  -> tclTHEN introf
                        (tclTHENS 
 			  (tclTHEN case_last clear_last)
-			  (List.map intro_pattern l)))
-    | ConjPat l  -> (tclTHEN introf
-                       (tclTHEN (tclTHEN  case_last clear_last)
-                          (intros_pattern l)))
+			  (List.map intro_pattern l))
+    | ConjPat l  ->
+        tclTHENSEQ [introf; case_last; clear_last; intros_pattern l]
     | ListPat l  ->  intros_pattern l
 
 and intros_pattern l = tclMAP intro_pattern l
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d2d2dadd5e..be301af0ea 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -47,16 +47,17 @@ open Coqlib
    Eduardo Gimenez (30/3/98).
 *)
 
-let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))))
+let clear_last = (tclLAST_HYP (fun c -> (clear [destVar c])))
 
 let mkBranches = 
-        (tclTHEN  intro 
-        (tclTHEN (tclLAST_HYP h_simplest_elim)
-        (tclTHEN  clear_last
-        (tclTHEN  intros 
-        (tclTHEN (tclLAST_HYP h_simplest_case)
-        (tclTHEN  clear_last
-                  intros))))))
+  tclTHENSEQ
+    [intro; 
+     tclLAST_HYP h_simplest_elim;
+     clear_last;
+     intros ;
+     tclLAST_HYP h_simplest_case;
+     clear_last;
+     intros]
 
 let solveRightBranch  = (tclTHEN h_simplest_right h_discrConcl)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 985db43022..763ca14c3c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -541,7 +541,7 @@ let discr id gls =
 	 errorlabstrm "discr" (str" Not a discriminable equality")
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "ee") gls in
-	 let e_env = push_named_decl (e,None,t) env in
+	 let e_env = push_named (e,None,t) env in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (indt,_) = find_mrectype env sigma t in 
@@ -790,7 +790,7 @@ let inj id gls =
 	   (str"Nothing to do, it is an equality between convertible terms")
     | Inr posns ->
 	let e = pf_get_new_id (id_of_string "e") gls in
-	let e_env = push_named_decl (e,None,t) env in
+	let e_env = push_named (e,None,t) env in
 	let injectors =
 	  map_succeed
 	    (fun (cpath,t1_0,t2_0) ->
@@ -844,7 +844,7 @@ let decompEqThen ntac id gls =
   (match find_positions env sigma t1 t2 with
      | Inl (cpath, (_,dirn), _) ->
 	 let e = pf_get_new_id (id_of_string "e") gls in
-	 let e_env = push_named_decl (e,None,t) env in
+	 let e_env = push_named (e,None,t) env in
 	 let discriminator =
 	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
 	 let (pf, absurd_term) =
@@ -858,7 +858,7 @@ let decompEqThen ntac id gls =
 	   (str"Nothing to do, it is an equality between convertible terms")
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
-	  let e_env = push_named_decl (e,None,t) env in
+	  let e_env = push_named (e,None,t) env in
 	  let injectors =
 	    map_succeed
 	      (fun (cpath,t1_0,t2_0) ->
@@ -873,7 +873,7 @@ let decompEqThen ntac id gls =
 	  if injectors = [] then
 	    errorlabstrm "Equality.decompEqThen" 
               (str "Discriminate failed to decompose the equality");
-	  ((tclTHEN
+	  (tclTHEN
 	      (tclMAP (fun (injfun,resty) ->
 			 let pf = applist(lbeq.congr (),
 					  [t;resty;injfun;t1;t2;
@@ -882,7 +882,7 @@ let decompEqThen ntac id gls =
 			 ((tclTHENS (cut ty) 
 			     ([tclIDTAC;refine pf]))))
 		 (List.rev injectors))
-	      (ntac (List.length injectors))))
+	      (ntac (List.length injectors)))
 	  gls))
 
 let decompEq = decompEqThen (fun x -> tclIDTAC)
@@ -1212,7 +1212,7 @@ let general_rewrite_in lft2rgt id (c,lb) gls =
 			(reduce (Pattern [(list_int nb_occ 1 [],l2,
 					   pf_type_of gls l2)]) []))
 		     (general_rewrite_bindings lft2rgt (c,lb))) 
-		  [(tclTHEN (clear_one id) (introduction id))]) gls)
+		  [(tclTHEN (clear [id]) (introduction id))]) gls)
 
 let dyn_rewrite_in lft2rgt = function
   | [Identifier id;(Command com);(Bindings binds)] -> 
@@ -1699,89 +1699,3 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
         (fun l -> validation_gen nlvalid l)
     in
     (repackage sigr gl,validation_fun)
-
-(*Collects the arguments of AutoRewrite ast node*)
-(*let dyn_autorewrite largs=
-  let rec explicit_base largs =
-    let tacargs = List.map cvt_arg largs in 
-    List.map 
-      (function
-	 | Redexp ("LR", [Coqast.Node(_,"Command", [ast])]) -> ast, true
-	 | Redexp ("RL", [Coqast.Node(_,"Command", [ast])]) -> ast, false
-	 | _ -> anomaly "Equality.explicit_base") 
-      tacargs
-  and list_bases largs =
-    let tacargs = List.map cvt_arg largs in 
-    List.map 
-      (function 
-	 | Redexp ("ByName", [Coqast.Nvar(_,s)]) -> 
-	     By_name (id_of_string s)
-	 | Redexp ("Explicit", l) ->
-	     Explicit (explicit_base l)
-	 | _ -> anomaly "Equality.list_bases") 
-      tacargs
-  and int_arg=function
-    | [(Integer n)] -> n
-    | _ -> anomalylabstrm "dyn_autorewrite" 
-	  (str "Bad call of int_arg (not an INTEGER)")
-  and list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
-    (orest,evorest) (depth,evdepth) = function
-      | [] -> (lstep,ostep,lrest,orest,depth)
-      | (Redexp (s,l))::tail ->
-	  if s="Step" & not evstep then
-            list_args_rest ((List.map Tacinterp.interp l),true) (ostep,evostep)
-              (lrest,evrest) (orest,evorest) (depth,evdepth) tail
-	  else if s="SolveStep" & not evostep then
-            list_args_rest (lstep,evstep) (Solve,true) (lrest,evrest)
-              (orest,evorest) (depth,evdepth) tail
-	  else if s="Use" & not evostep then
-            list_args_rest (lstep,evstep) (Use,true) (lrest,evrest) 
-	      (orest,evorest) (depth,evdepth) tail
-	  else if s="All" & not evostep then
-            list_args_rest (lstep,evstep) (All,true) (lrest,evrest) 
-	      (orest,evorest) (depth,evdepth) tail
-	  else if s="Rest" & not evrest then
-            list_args_rest (lstep,evstep) (ostep,evostep) 
-	      ((List.map Tacinterp.interp l),true) (orest,evorest) 
-	      (depth,evdepth) tail
-	  else if s="SolveRest" & not evorest then
-            list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
-              (false,true) (depth,evdepth) tail
-	  else if s="Cond" & not evorest then
-            list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
-              (true,true) (depth,evdepth) tail
-	  else if s="Depth" & not evdepth then
-            (let dth = int_arg (List.map cvt_arg l) in
-             if dth > 0 then
-               list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest)
-		 (orest,evorest) (dth,true) tail
-             else
-               errorlabstrm "dyn_autorewrite" 
-		 (str "Depth value lower or equal to 0"))
-	  else
-            anomalylabstrm "dyn_autorewrite" 
-	      (str "Bad call of list_args_rest")
-      | _ -> 
-	  anomalylabstrm "dyn_autorewrite" 
-	    (str "Bad call of list_args_rest")
-  and list_args = function
-    | (Redexp (s,lbases))::tail ->
-	if s = "BaseList" then
-          (let (lstep,ostep,lrest,orest,depth) = 
-	     list_args_rest ([],false) (Solve,false) ([],false) (false,false) 
-	       (100,false) tail
-           in
-           autorewrite (list_bases lbases) 
-	     (if lstep = [] then None else Some lstep) 
-	     ostep (if lrest=[] then None else Some lrest) orest depth)
-	else
-          anomalylabstrm "dyn_autorewrite" 
-	    (str "Bad call of list_args (not a BaseList tagged REDEXP)")
-    | _ ->
-	anomalylabstrm "dyn_autorewrite" 
-	  (str "Bad call of list_args (not a REDEXP)")
-  in
-  list_args largs*)
-
-(*Adds and hides the AutoRewrite tactic*)
-(*let h_autorewrite = hide_tactic "AutoRewrite" dyn_autorewrite*)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 32fc1a365f..b372b8bdf2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -34,6 +34,41 @@ open Equality
 open Typing
 open Pattern
 
+let collect_meta_variables c = 
+  let rec collrec acc c = match kind_of_term c with
+    | Meta mv -> mv::acc
+    | _ -> fold_constr collrec acc c
+  in 
+  collrec [] c
+
+let check_no_metas clenv ccl =
+  if occur_meta ccl then
+    let metas = List.map (fun n -> Intmap.find n clenv.namenv)
+		  (collect_meta_variables ccl) in
+    errorlabstrm "inversion" 
+      (str ("Cannot find an instantiation for variable"^
+	       (if List.length metas = 1 then " " else "s ")) ++
+	 prlist_with_sep pr_coma pr_id metas
+	 (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *))
+
+let dest_match_eq gls eqn =
+  try 
+    pf_matches gls (Coqlib.build_coq_eq_pattern ()) eqn
+  with PatternMatchingFailure -> 
+    (try 
+       pf_matches gls (Coqlib.build_coq_eqT_pattern ()) eqn
+     with PatternMatchingFailure -> 
+       (try 
+	  pf_matches gls (Coqlib.build_coq_idT_pattern ()) eqn
+        with PatternMatchingFailure ->
+	  errorlabstrm "dest_match_eq" 
+	    (str "no primitive equality here")))
+
+let var_occurs_in_pf gl id =
+  let env = pf_env gl in
+  occur_var env id (pf_concl gl) or
+  List.exists (occur_var_in_decl env id) (pf_hyps gl)
+
 (* [make_inv_predicate (ity,args) C]
   
    is given the inductive type, its arguments, both the global
@@ -60,23 +95,6 @@ open Pattern
 
  *)
 
-let dest_match_eq gls eqn =
-  try 
-    pf_matches gls (Coqlib.build_coq_eq_pattern ()) eqn
-  with PatternMatchingFailure -> 
-    (try 
-       pf_matches gls (Coqlib.build_coq_eqT_pattern ()) eqn
-     with PatternMatchingFailure -> 
-       (try 
-	  pf_matches gls (Coqlib.build_coq_idT_pattern ()) eqn
-        with PatternMatchingFailure ->
-	  errorlabstrm "dest_match_eq" 
-	    (str "no primitive equality here")))
-    
-(* Environment management *)
-let push_rels vars env =
-  List.fold_right push_rel vars env
-
 type inversion_status = Dep of constr option | NoDep
 
 let compute_eqn env sigma n i ai =
@@ -93,7 +111,7 @@ let make_inv_predicate env sigma ind id status concl =
 	  let hyps_arity,_ = get_arity env indf in
 	  (hyps_arity,concl)
       | Dep dflt_concl ->
-	  if not (dependent (mkVar id) concl) then
+	  if not (occur_var env id concl) then
 	    errorlabstrm "make_inv_predicate"
               (str "Current goal does not depend on " ++ pr_id id);
           (* We abstract the conclusion of goal with respect to
@@ -111,7 +129,7 @@ let make_inv_predicate env sigma ind id status concl =
 	  (hyps,lift nrealargs bodypred)
   in
   let nhyps = List.length hyps in
-  let env' = push_rels hyps env in
+  let env' = push_rel_context hyps env in
   let realargs' = List.map (lift nhyps) realargs in
   let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in
   (* Now the arity is pushed, and we need to construct the pairs
@@ -178,8 +196,6 @@ let make_inv_predicate env sigma ind id status concl =
    the equality, using Injection and Discriminate, and applying it to
    the concusion *)
 
-let introsReplacing = intros_replacing (* déplacé *)
-
 (* Computes the subset of hypothesis in the local context whose
    type depends on t (should be of the form (mkVar id)), then
    it generalizes them, applies tac to rewrite all occurrencies of t,
@@ -196,45 +212,12 @@ let rec dependent_hyps id idlist sign =
   in 
   dep_rec idlist 
 
-let generalizeRewriteIntros tac depids id gls = 
-  let dids = dependent_hyps id depids (pf_env gls) in
-  (tclTHEN (bring_hyps dids)
-     (tclTHEN tac
-	(introsReplacing (ids_of_named_context dids))))
-  gls
-
-let var_occurs_in_pf gl id =
-  let env = pf_env gl in
-  occur_var env id (pf_concl gl) or
-  List.exists (occur_var_in_decl env id) (pf_hyps gl)
-
 let split_dep_and_nodep hyps gl =
   List.fold_right 
     (fun (id,_,_ as d) (l1,l2) ->
        if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2))
     hyps ([],[])
 
-(*
-let split_dep_and_nodep hyps gl =
-  let env = pf_env gl in
-  let cl = pf_concl gl in
-  let l1,l2 =
-    List.fold_left
-      (fun (l1,l2) (id,_,_ as d) ->
-         if
-           occur_var env id cl
-           or List.exists (occur_var_in_decl env id) hyps
-           or List.exists (fun (id,_,_) -> occur_var_in_decl env id d) l1
-         then (d::l1,l2)
-         else (l1,d::l2))
-      ([],[]) hyps
-  in (List.rev l1,List.rev l2)
-*)
-
-(* invariant: ProjectAndApply is responsible for erasing the clause
-   which it is given as input
-   It simplifies the clause (an equality) to use it as a rewrite rule and then
-   erases the result of the simplification. *)
 
 let dest_eq gls t =
   match dest_match_eq gls t with
@@ -242,6 +225,16 @@ let dest_eq gls t =
         (x,pf_whd_betadeltaiota gls y, pf_whd_betadeltaiota gls z)
     | _ -> error "dest_eq: should be an equality"
 
+let generalizeRewriteIntros tac depids id gls = 
+  let dids = dependent_hyps id depids (pf_env gls) in
+  (tclTHENSEQ
+    [bring_hyps dids; tac; intros_replacing (ids_of_named_context dids)])
+  gls
+
+(* invariant: ProjectAndApply is responsible for erasing the clause
+   which it is given as input
+   It simplifies the clause (an equality) to use it as a rewrite rule and then
+   erases the result of the simplification. *)
 (* invariant: ProjectAndApplyNoThining simplifies the clause (an equality) .
    If it can discriminate then the goal is proved, if not tries to use it as
    a rewrite rule. It erases the clause which is given as input *)
@@ -266,57 +259,56 @@ let projectAndApply thin id depids gls =
   match (thin, kind_of_term t1, kind_of_term t2) with
     | (true, Var id1,  _) ->
         generalizeRewriteIntros
-          (tclTHEN (subst_hyp_LR id) (clear_clause id)) depids id1 gls
+          (tclTHEN (subst_hyp_LR id) (clear [id])) depids id1 gls
     | (false, Var id1,  _) ->
         generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls
     | (true, _ , Var id2) ->
         generalizeRewriteIntros
-          (tclTHEN (subst_hyp_RL id) (clear_clause id)) depids id2 gls
+          (tclTHEN (subst_hyp_RL id) (clear [id])) depids id2 gls
     | (false, _ , Var id2) ->
         generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls
     | (true, _, _) ->
         let deq_trailer neqns =
           tclDO neqns
-            (tclTHEN intro (tclTHEN subst_hyp (onLastHyp clear_clause)))
+            (tclTHENSEQ
+              [intro; subst_hyp; onLastHyp (fun id -> clear [id])])
         in 
-	(tclTHEN (tclTRY (dEqThen deq_trailer (Some id))) (clear_one id)) gls
+	(tclTHEN (tclTRY (dEqThen deq_trailer (Some id))) (clear [id])) gls
     | (false, _, _) -> 
         let deq_trailer neqns = tclDO neqns (tclTHEN intro subst_hyp) in 
-	(tclTHEN (dEqThen deq_trailer (Some id)) (clear_one id)) gls
+	(tclTHEN (dEqThen deq_trailer (Some id)) (clear [id])) gls
 
 (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
    soi-meme (proposition de Valerie). *)
-let case_trailer_gene othin neqns ba gl =
+let rewrite_equations_gene othin neqns ba gl =
   let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
   let rewrite_eqns =
     match othin with
       | Some thin ->
           onLastHyp
             (fun last ->
-               (tclTHEN
-                  (tclDO neqns
+              tclTHENSEQ
+                [tclDO neqns
                      (tclTHEN intro
                         (onLastHyp
                            (fun id ->
-                              tclTRY (projectAndApply thin id depids)))))
-		  (tclTHEN
-                     (onHyps (compose List.rev (afterHyp last)) bring_hyps)
-                     (onHyps (afterHyp last)
-                        (compose clear ids_of_named_context)))))
+                              tclTRY (projectAndApply thin id depids))));
+                 onHyps (compose List.rev (afterHyp last)) bring_hyps;
+                 onHyps (afterHyp last)
+                   (compose clear ids_of_named_context)])
       | None -> tclIDTAC
   in
-  (tclTHEN (tclDO neqns intro)
-     (tclTHEN (bring_hyps nodepids)
-	(tclTHEN (clear_clauses (ids_of_named_context nodepids))
-	   (tclTHEN (onHyps (compose List.rev (nLastHyps neqns)) bring_hyps)
-	      (tclTHEN (onHyps (nLastHyps neqns)
-                          (compose clear_clauses ids_of_named_context))
-		 (tclTHEN rewrite_eqns
-		    (tclMAP (fun (id,_,_ as d) ->
-			       (tclORELSE (clear_clause id)
-				  (tclTHEN (bring_hyps [d])
-				     (clear_one id))))
-		       depids)))))))
+  (tclTHENSEQ
+    [tclDO neqns intro;
+     bring_hyps nodepids;
+     clear (ids_of_named_context nodepids);
+     onHyps (compose List.rev (nLastHyps neqns)) bring_hyps;
+     onHyps (nLastHyps neqns) (compose clear ids_of_named_context);
+     rewrite_eqns;
+     tclMAP (fun (id,_,_ as d) ->
+               (tclORELSE (clear [id])
+                 (tclTHEN (bring_hyps [d]) (clear [id]))))
+       depids])
   gl
 
 (* Introduction of the equations on arguments
@@ -324,49 +316,40 @@ let case_trailer_gene othin neqns ba gl =
      None: the equations are introduced, but not rewritten
      Some thin: the equations are rewritten, and cleared if thin is true *)
 
-let case_trailer othin neqns ba gl =
+let rewrite_equations othin neqns ba gl =
   let (depids,nodepids) = split_dep_and_nodep ba.assums gl in
   let rewrite_eqns =
     match othin with
       | Some thin ->
-          (tclTHEN (onHyps (compose List.rev (nLastHyps neqns)) bring_hyps)
-             (tclTHEN (onHyps (nLastHyps neqns) 
-                         (compose clear_clauses ids_of_named_context))
-		(tclTHEN
-		   (tclDO neqns
-                      (tclTHEN intro
-			 (onLastHyp
-			    (fun id -> 
-			       tclTRY (projectAndApply thin id depids)))))
-		   (tclTHEN (tclDO (List.length nodepids) intro)
-		      (tclMAP (fun (id,_,_) -> 
-				 tclTRY (clear_clause id)) depids)))))
+          tclTHENSEQ
+            [onHyps (compose List.rev (nLastHyps neqns)) bring_hyps;
+             onHyps (nLastHyps neqns) (compose clear ids_of_named_context);
+	     tclDO neqns
+               (tclTHEN intro
+		 (onLastHyp
+		   (fun id -> tclTRY (projectAndApply thin id depids))));
+	     tclDO (List.length nodepids) intro;
+	     tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids]
       | None -> tclIDTAC
   in
-  (tclTHEN (tclDO neqns intro)
-     (tclTHEN (bring_hyps nodepids)
-	(tclTHEN (clear_clauses (ids_of_named_context nodepids))
-	   rewrite_eqns)))
+  (tclTHENSEQ
+    [tclDO neqns intro;
+     bring_hyps nodepids;
+     clear (ids_of_named_context nodepids);
+     rewrite_eqns])
   gl
 
-let collect_meta_variables c = 
-  let rec collrec acc c = match kind_of_term c with
-    | Meta mv -> mv::acc
-    | _ -> fold_constr collrec acc c
-  in 
-  collrec [] c
+let rewrite_equations_tac (gene, othin) id neqns ba =
+  let tac =
+    if gene then rewrite_equations_gene othin neqns ba
+    else rewrite_equations othin neqns ba in
+  if othin = Some true (* if Inversion_clear, clear the hypothesis *) then 
+    tclTHEN tac (tclTRY (clear [id]))
+  else 
+    tac
 
-let check_no_metas clenv ccl =
-  if occur_meta ccl then
-    let metas = List.map (fun n -> Intmap.find n clenv.namenv)
-		  (collect_meta_variables ccl) in
-    errorlabstrm "res_case_then" 
-      (str ("Cannot find an instantiation for variable"^
-	       (if List.length metas = 1 then " " else "s ")) ++
-	 prlist_with_sep pr_coma pr_id metas
-	 (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *))
 
-let res_case_then gene thin indbinding id status gl =
+let raw_inversion inv_kind indbinding id status gl =
   let env = pf_env gl and sigma = project gl in
   let c = mkVar id in
   let (wc,kONT) = startWalk gl in
@@ -379,7 +362,7 @@ let res_case_then gene thin indbinding id status gl =
   let (IndType (indf,realargs) as indt) =
     try find_rectype env sigma ccl
     with Not_found ->
-      errorlabstrm "res_case_then"
+      errorlabstrm "raw_inversion"
 	(str ("The type of "^(string_of_id id)^" is not inductive")) in
   let (elim_predicate,neqns) =
     make_inv_predicate env sigma indt id status (pf_concl gl) in
@@ -389,12 +372,9 @@ let res_case_then gene thin indbinding id status gl =
     else 
       applist(elim_predicate,realargs),case_nodep_then_using 
   in
-  let case_trailer_tac =
-    if gene then case_trailer_gene thin neqns else case_trailer thin neqns
-  in
   (tclTHENS
      (true_cut_anon cut_concl)
-     [case_tac (introCaseAssumsThen case_trailer_tac)
+     [case_tac (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
         (Some elim_predicate) ([],[]) newc;
       onLastHyp
         (fun id ->
@@ -435,15 +415,12 @@ let wrap_inv_error id = function
   | Not_found  ->  errorlabstrm "Inv" (not_found_message [id]) 
   | e -> raise e
 
-let inv gene thin status id =
-  let inv_tac = res_case_then gene thin [] id status in
-  let tac =
-    if thin = Some true (* if Inversion_clear, clear the hypothesis *) then 
-      tclTHEN inv_tac (tclTRY (clear_clause id))
-    else 
-      inv_tac
-  in 
-  fun gls -> try tac gls with e -> wrap_inv_error id e
+(* The most general inversion tactic *)
+let inversion inv_kind status id gls =
+  try (raw_inversion inv_kind [] id status) gls
+  with e -> wrap_inv_error id e
+
+(* Specializing it... *)
 
 let hinv_kind = Quoted_string "HalfInversion"
 let inv_kind = Quoted_string "Inversion"
@@ -460,7 +437,9 @@ let (half_inv_tac, inv_tac, inv_clear_tac) =
     hide_tactic "Inv"
       (function
 	 | ic :: [id_or_num] ->
-	     tactic_try_intros_until (inv false (com_of_id ic) NoDep) id_or_num
+	     tactic_try_intros_until
+               (inversion (false, com_of_id ic) NoDep)
+               id_or_num
 	 | l -> bad_tactic_args "Inv" l)
   in
   ((fun id -> gentac [hinv_kind; Identifier id]),
@@ -473,7 +452,7 @@ let named_inv =
   let gentac =
     hide_tactic "NamedInv"
       (function
-	 | [ic; Identifier id] -> inv true (com_of_id ic) NoDep id
+	 | [ic; Identifier id] -> inversion (true, com_of_id ic) NoDep id
 	 | l -> bad_tactic_args "NamedInv" l)
   in 
   (fun ic id -> gentac [ic; Identifier id])
@@ -484,7 +463,8 @@ let (half_dinv_tac, dinv_tac, dinv_clear_tac) =
     hide_tactic "DInv"
       (function
 	 | ic :: [id_or_num] ->
-	     tactic_try_intros_until (inv false (com_of_id ic) (Dep None))
+	     tactic_try_intros_until
+               (inversion (false, com_of_id ic) (Dep None))
 	       id_or_num
 	 | l -> bad_tactic_args "DInv" l)
   in
@@ -500,12 +480,13 @@ let (half_dinv_with, dinv_with, dinv_clear_with) =
 	 | [ic; id_or_num; Command com] ->
 	     tactic_try_intros_until
                (fun id gls -> 
-		  inv false (com_of_id ic)
-		    (Dep (Some (pf_interp_constr gls com))) id gls)
+		 inversion (false, com_of_id ic)
+		   (Dep (Some (pf_interp_constr gls com))) id gls)
 	       id_or_num
 	 | [ic; id_or_num; Constr c] ->
 	     tactic_try_intros_until
-               (fun id gls -> inv false (com_of_id ic) (Dep (Some c)) id gls)
+               (fun id gls ->
+                 inversion (false, com_of_id ic) (Dep (Some c)) id gls)
 	       id_or_num
 	 | l -> bad_tactic_args "DInvWith" l)
   in
@@ -525,14 +506,13 @@ let invIn com id ids gls =
       nb_prod (pf_concl gls) - (List.length hyps + nb_prod_init)
     in 
     if nb_of_new_hyp < 1 then 
-      introsReplacing ids gls
+      intros_replacing ids gls
     else 
-      tclTHEN (tclDO nb_of_new_hyp intro) (introsReplacing ids) gls
+      tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids) gls
   in
   try 
-    (tclTHEN (bring_hyps hyps)
-       (tclTHEN (inv false com NoDep id)
-          (intros_replace_ids)))
+    (tclTHENSEQ
+      [bring_hyps hyps; inversion (false, com) NoDep id; intros_replace_ids])
     gls
   with e -> wrap_inv_error id e
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1344e009b6..3433618153 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -137,11 +137,11 @@ let rec add_prods_sign env sigma t =
     | Prod (na,c1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named_decl (id,None,c1) env) sigma b'
+        add_prods_sign (push_named (id,None,c1) env) sigma b'
     | LetIn (na,c1,t1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named_decl (id,Some c1,t1) env) sigma b'
+        add_prods_sign (push_named (id,Some c1,t1) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates wether the inversion lemma is dependent or not.
@@ -186,7 +186,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_betadeltaiota env sigma pty in
-  let extenv = push_named_decl (p,None,npty) env in
+  let extenv = push_named (p,None,npty) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
diff --git a/tactics/refine.ml b/tactics/refine.ml
index cc90f4b23f..7567ae35eb 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -150,7 +150,7 @@ let rec compute_metamap env gmm c = match kind_of_term c with
    *    où x est une variable FRAICHE *)
   | Lambda (name,c1,c2) ->
       let v = fresh env name in
-      let env' = push_named_decl (v,None,c1) env in
+      let env' = push_named (v,None,c1) env in
       begin match compute_metamap env' gmm (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
@@ -164,7 +164,7 @@ let rec compute_metamap env gmm c = match kind_of_term c with
       if occur_meta c1 then 
 	error "Refine: body of let-in cannot contain existentials";
       let v = fresh env name in
-      let env' = push_named_decl (v,Some c1,t1) env in
+      let env' = push_named (v,Some c1,t1) env in
       begin match compute_metamap env' gmm (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 70716cde2d..78e80a0ec0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -48,6 +48,9 @@ let tclDO            = Tacmach.tclDO
 let tclPROGRESS      = Tacmach.tclPROGRESS
 let tclWEAK_PROGRESS = Tacmach.tclWEAK_PROGRESS
 
+(* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
+let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
+
 (* map_tactical f [x1..xn] = (f x1);(f x2);...(f xn) *)
 (* tclMAP f [x1..xn] = (f x1);(f x2);...(f xn) *)
 let tclMAP tacfun l = 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index a984d791f9..af0ea2a66b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -29,6 +29,7 @@ val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 val tclTHENL         : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
 val tclTHENSi        : tactic -> tactic list -> (int -> tactic) -> tactic
+val tclTHENSEQ       : tactic list -> tactic
 val tclREPEAT        : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
 val tclTRY           : tactic -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b338e1c702..5623e38996 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -739,7 +739,7 @@ let letin_abstract id c (occ_ccl,occ_hyps) gl =
   let abstract ((depdecls,marks as accu),lhyp) (hyp,_,_ as d) =
     try
       let occ = if everywhere then [] else List.assoc hyp occ_hyps in
-      let newdecl = subst_term_occ_decl occ c d in
+      let newdecl = subst_term_occ_decl env occ c d in
       if d = newdecl then
 	if not everywhere then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 	else (accu, Some hyp)
@@ -754,7 +754,7 @@ let letin_abstract id c (occ_ccl,occ_hyps) gl =
   let occ_ccl = if everywhere then Some [] else occ_ccl in
   let ccl = match occ_ccl with
     | None -> pf_concl gl
-    | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl))
+    | Some occ -> subst1 (mkVar id) (subst_term_occ env occ c (pf_concl gl))
   in
   (depdecls,marks,ccl)
 
@@ -874,7 +874,6 @@ let dyn_assumption = function
  * goal. *)                                                               
 
 let clear ids gl    = thin ids gl
-let clear_one id gl = clear [id] gl
 let dyn_clear = function
   | [Clause ids] ->
       let out = function InHyp id -> id | _ -> assert false in
@@ -888,20 +887,6 @@ let dyn_clear_body = function
       clear_body (List.map out ids)
   | l -> bad_tactic_args "clear_body" l
 
-(* Clears a list of identifiers clauses form the context *)
-(*
-let clear_clauses clsl =
-  clear (List.map 
-           (function 
-	      | Some id -> id
-              | None    -> error "ThinClauses") clsl)
-*)
-let clear_clauses = clear
-
-(* Clears one identifier clause from the context *)
-
-let clear_clause cls = clear_clauses [cls]
-
 
 (*   Takes a list of booleans, and introduces all the variables 
  *  quantified in the goal which are associated with a value
@@ -911,7 +896,8 @@ let rec intros_clearing = function
   | []          -> tclIDTAC
   | (false::tl) -> tclTHEN intro (intros_clearing tl)
   | (true::tl)  ->
-      tclTHENLIST [ intro; onLastHyp clear_clause; intros_clearing tl]
+      tclTHENLIST
+        [ intro; onLastHyp (fun id -> clear [id]); intros_clearing tl]
 
 (* Adding new hypotheses  *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 568ce9c484..3f611f831d 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -152,15 +152,11 @@ val pattern_option    :
 (*s Modification of the local context. *)
 
 val clear         : identifier list -> tactic
-val clear_one     : identifier -> tactic
 val dyn_clear     : tactic_arg list -> tactic
 
 val clear_body    : identifier list -> tactic
 val dyn_clear_body : tactic_arg list -> tactic
 
-val clear_clauses : identifier list -> tactic
-val clear_clause  : identifier -> tactic
-
 val new_hyp       : int option ->constr -> constr substitution -> tactic
 val dyn_new_hyp   : tactic_arg list -> tactic