Restructuration fonctions de réécriture depuis égalité dépendante; factorisation cut_replacing

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

4 files changed, 159 insertions, 175 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index eb90fa213..fed587e4e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -39,6 +39,7 @@ open Coqlib
 open Vernacexpr
 open Setoid_replace
 open Declarations
+open Indrec
 
 (* Rewriting tactics *)
 
@@ -47,10 +48,28 @@ open Declarations
    with type (A:<sort>)(x:A)(P:A->Prop)(P x)->(y:A)(eqname A y x)->(P y).
    If another equality myeq is introduced, then corresponding theorems
    myeq_ind_r, myeq_rec_r and myeq_rect_r have to be proven. See below.
-   -- Eduardo (19/8/97
+   -- Eduardo (19/8/97)
 *)
 
-let general_rewrite_bindings lft2rgt (c,l) gl =
+let general_s_rewrite_clause = function
+  | None -> general_s_rewrite
+  | Some id -> general_s_rewrite_in id
+
+(* Ad hoc asymmetric general_elim_clause *)
+let general_elim_clause cls c elim = match cls with
+  | None ->
+      (* was tclWEAK_PROGRESS which only fails for tactics generating one 
+         subgoal and did not fail for useless conditional rewritings generating
+         an extra condition *)
+      tclNOTSAMEGOAL (general_elim c elim ~allow_K:false)
+  | Some id ->
+      general_elim_in id c elim 
+
+let elimination_sort_of_clause = function
+  | None -> elimination_sort_of_goal
+  | Some id -> elimination_sort_of_hyp id
+
+let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
   let ctype = pf_type_of gl c in 
   let env = pf_env gl in
   let sigma = project gl in 
@@ -58,21 +77,27 @@ let general_rewrite_bindings lft2rgt (c,l) gl =
   match match_with_equation t with
     | None -> 
 	if l = NoBindings
-	then general_s_rewrite lft2rgt c [] gl
+	then general_s_rewrite_clause cls lft2rgt c [] gl
 	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_of_inductive hdcncl in 
-	let suffix = Indrec.elimination_suffix (elimination_sort_of_goal gl)in
+	let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+        let dir = if cls=None then lft2rgt else not lft2rgt in
+        let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
         let elim =
-	  if lft2rgt then
-            pf_global gl (id_of_string (hdcncls^suffix^"_r"))
-          else
-	    pf_global gl (id_of_string (hdcncls^suffix))
+	  try pf_global gl (id_of_string rwr_thm)
+          with Not_found ->
+            error ("Cannot find rewrite principle "^rwr_thm)
         in 
-	tclNOTSAMEGOAL (general_elim (c,l) (elim,NoBindings) ~allow_K:false) gl
-   (* was tclWEAK_PROGRESS which only fails for tactics generating one subgoal 
-      and did not fail for useless conditional rewritings generating an
-      extra condition *)
+	general_elim_clause cls (c,l) (elim,NoBindings) gl
+
+let general_rewrite_bindings = general_rewrite_bindings_clause None
+let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings)
+
+let general_rewrite_bindings_in l2r id =
+  general_rewrite_bindings_clause (Some id) l2r
+let general_rewrite_in l2r id c = 
+  general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
 
 (* Conditional rewriting, the success of a rewriting is related 
    to the resolution of the conditions by a given tactic *)
@@ -81,47 +106,22 @@ let conditional_rewrite lft2rgt tac (c,bl) =
   tclTHENSFIRSTn (general_rewrite_bindings lft2rgt (c,bl))
     [|tclIDTAC|] (tclCOMPLETE tac)
 
-let general_rewrite lft2rgt c = general_rewrite_bindings lft2rgt (c,NoBindings)
-
 let rewriteLR_bindings = general_rewrite_bindings true
 let rewriteRL_bindings = general_rewrite_bindings false
 
 let rewriteLR = general_rewrite true
 let rewriteRL = general_rewrite false
 
-(* The Rewrite in tactic *)
-let general_rewrite_in lft2rgt id (c,l) gl =
-  let ctype = pf_type_of gl c in 
-  let env = pf_env gl in
-  let sigma = project gl in 
-  let _,t = splay_prod env sigma ctype in
-  match match_with_equation t with
-    | None -> (* Do not deal with setoids yet *) 
-	if l = NoBindings
-	then general_s_rewrite_in id lft2rgt c [] gl
-	else error "The term provided does not end with an equation" 
-    | Some (hdcncl,_) -> 
-        let hdcncls = string_of_inductive hdcncl in 
-	let suffix =
-          Indrec.elimination_suffix (elimination_sort_of_hyp id gl) in
-        let rwr_thm =
-          if lft2rgt then hdcncls^suffix else hdcncls^suffix^"_r" in
-        let elim =
-	  try pf_global gl (id_of_string rwr_thm)
-          with Not_found ->
-            error ("Cannot find rewrite principle "^rwr_thm) in 
-	general_elim_in id (c,l) (elim,NoBindings) gl
-
-let rewriteLRin = general_rewrite_in true
-let rewriteRLin = general_rewrite_in false
+let rewriteLRin_bindings = general_rewrite_bindings_in true
+let rewriteRLin_bindings = general_rewrite_bindings_in false
 
 let conditional_rewrite_in lft2rgt id tac (c,bl) = 
-  tclTHENSFIRSTn (general_rewrite_in lft2rgt id (c,bl))
+  tclTHENSFIRSTn (general_rewrite_bindings_in lft2rgt id (c,bl))
     [|tclIDTAC|] (tclCOMPLETE tac)
 
 let rewriteRL_clause = function
   | None -> rewriteRL_bindings
-  | Some id -> rewriteRLin id
+  | Some id -> rewriteRLin_bindings id
 
 (* Replacing tactics *)
 
@@ -827,9 +827,8 @@ let swapEquandsInConcl gls =
   refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
 
 let swapEquandsInHyp id gls =
-  ((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id)))
-      ([tclIDTAC;
-      	(tclTHEN (swapEquandsInConcl) (exact_no_check (mkVar id)))]))) gls
+  cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))
+    (tclTHEN swapEquandsInConcl) gls
 
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. It yields the boolean true wether
@@ -940,9 +939,10 @@ let subst_tuple_term env sigma dep_pair b =
      |- (P e1)
      |- (eq T e1 e2)
  *)
+
 (* Redondant avec Replace ! *)
 
-let substInConcl_RL eqn gls =
+let cutSubstInConcl_RL eqn gls =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in
   let body = subst_tuple_term (pf_env gls) (project gls) e2 (pf_concl gls) in
   assert (dependent (mkRel 1) body);
@@ -953,28 +953,26 @@ let substInConcl_RL eqn gls =
      |- (P e2)
      |- (eq T e1 e2)
  *)
-let substInConcl_LR eqn gls =
-  (tclTHENS (substInConcl_RL (swap_equands gls eqn))
+let cutSubstInConcl_LR eqn gls =
+  (tclTHENS (cutSubstInConcl_RL (swap_equands gls eqn))
      ([tclIDTAC;
        swapEquandsInConcl])) gls
 
-let substInConcl l2r = if l2r then substInConcl_LR else substInConcl_RL
+let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL
 
-let substInHyp_LR eqn id gls =
+let cutSubstInHyp_LR eqn id gls =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in 
   let body = subst_term e1 (pf_get_hyp_typ gls id) in
   if not (dependent (mkRel 1) body) then errorlabstrm  "SubstInHyp" (mt ());
-  (tclTHENS (cut_replacing id (subst1 e2 body))
-     ([tclIDTAC;
-       (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2))
-          ([exact_no_check (mkVar id);tclIDTAC]))])) gls
+  cut_replacing id (subst1 e2 body)
+    (tclTHENFIRST (bareRevSubstInConcl lbeq body (t,e1,e2))) gls
 
-let substInHyp_RL eqn id gls =
-  (tclTHENS (substInHyp_LR (swap_equands gls eqn) id)
+let cutSubstInHyp_RL eqn id gls =
+  (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id)
      ([tclIDTAC;
        swapEquandsInConcl])) gls
 
-let substInHyp l2r = if l2r then substInHyp_LR else substInHyp_RL
+let cutSubstInHyp l2r = if l2r then cutSubstInHyp_LR else cutSubstInHyp_RL
 
 let try_rewrite tac gls =
   try 
@@ -987,77 +985,51 @@ let try_rewrite tac gls =
           (str "Cannot find a well-typed generalization of the goal that" ++
              str " makes the proof progress")
 
-let subst l2r eqn cls gls =
+let cutSubstClause l2r eqn cls gls =
   match cls with
-    | None ->    substInConcl l2r eqn gls
-    | Some id -> substInHyp l2r eqn id gls
+    | None ->    cutSubstInConcl l2r eqn gls
+    | Some id -> cutSubstInHyp l2r eqn id gls
 
-(* |- (P a)
- * SubstConcl_LR a=b 
- *  |- (P b)
- *  |- a=b
- *)
+let cutRewriteClause l2r eqn cls = try_rewrite (cutSubstClause l2r eqn cls)
+let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
+let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
-let substConcl l2r eqn gls = try_rewrite (subst l2r eqn None) gls
-let substConcl_LR = substConcl true
+let substClause l2r c cls gls =
+  let eq = pf_type_of gls c in
+  tclTHENS (cutSubstClause l2r eq cls) [tclIDTAC; exact_no_check c] gls
 
-(* id:(P a) |- G
- * SubstHyp a=b id
- *  id:(P b) |- G
- *  id:(P a) |-a=b
-*)
+let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
+let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
+let rewriteInConcl l2r c = rewriteClause l2r c None
 
-let hypSubst l2r id cls gls =
-  onClauses (function
-    | None -> 
-	(tclTHENS (substInConcl l2r (pf_get_hyp_typ gls id))
-	   ([tclIDTAC; exact_no_check (mkVar id)]))
-    | Some (hypid,_,_) -> 
-	(tclTHENS (substInHyp l2r (pf_get_hyp_typ gls id) hypid)
-	   ([tclIDTAC;exact_no_check (mkVar id)])))
-    cls gls
+(* Renaming scheme correspondence new name (old name)
 
-let hypSubst_LR = hypSubst true
+      give equality                    give proof of equality
 
-(* id:a=b |- (P a)
- * HypSubst id.
- *  id:a=b |- (P b)
- *)
-let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id onConcl) gls
-let substHypInConcl_LR = substHypInConcl true
+    / cutSubstClause (subst)          substClause (HypSubst on hyp)
+raw | cutSubstInHyp (substInHyp)      substInHyp (none)
+    \ cutSubstInConcl (substInConcl)  substInConcl (none) 
 
-(* id:a=b H:(P a) |- G
-   SubstHypInHyp id H.
-    id:a=b H:(P b) |- G
-*)
-(* |- (P b)
-   SubstConcl_RL a=b
-     |- (P a)
-     |- a=b
-*)
-let substConcl_RL = substConcl false
+    / cutRewriteClause (none)         rewriteClause (none)
+user| cutRewriteInHyp (substHyp)      rewriteInHyp (none)
+    \ cutRewriteInConcl (substConcl)  rewriteInConcl (substHypInConcl on hyp)
 
-(* id:(P b) |-G
-   SubstHyp_RL a=b id 
-      id:(P a) |- G
-      |- a=b  
+raw = raise typing error or PatternMatchingFailure
+user = raise user error specific to rewrite
 *)
-let substHyp l2r eqn id gls = try_rewrite (subst l2r eqn (Some id)) gls
-let substHyp_RL = substHyp false
 
+(* Summary of obsolete forms
+let substInConcl = cutSubstInConcl
+let substInHyp = cutSubstInHyp
+let hypSubst l2r id = substClause l2r (mkVar id)
+let hypSubst_LR = hypSubst true
 let hypSubst_RL = hypSubst false
-
-(* id:a=b |- (P b)
- * HypSubst id.
- * id:a=b |- (P a)
- *)
-let substHypInConcl_RL = substHypInConcl false
-
-(* id:a=b H:(P b) |- G
-   SubstHypInHyp id H.
-    id:a=b H:(P a) |- G
+let substHypInConcl l2r id = rewriteInConcl l2r (mkVar id)
+let substConcl = cutRewriteInConcl
+let substHyp = cutRewriteInHyp
 *)
 
+(**********************************************************************)
 (* Substitutions tactics (JCF) *)
 
 let unfold_body x gl =
@@ -1172,7 +1144,7 @@ let rewrite_assumption_cond_in faildir hyp gl =
       | [] -> error "No such assumption"
       | (id,_,t)::rest -> 
 	  (try let dir = faildir t gl in 
-	       general_rewrite_in dir hyp ((mkVar id),NoBindings) gl
+	       general_rewrite_in dir hyp (mkVar id) gl
 	   with Failure _ | UserError _ ->  arec rest)
    in arec (pf_hyps gl)
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 672c4014a..f511fe675 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -28,14 +28,24 @@ val find_eq_pattern : sorts -> sorts -> constr
 
 val general_rewrite_bindings : bool -> constr with_bindings -> tactic
 val general_rewrite          : bool -> constr -> tactic
+
+(* Obsolete, use [general_rewrite_bindings l2r]
 val rewriteLR_bindings       : constr with_bindings -> tactic
 val rewriteRL_bindings       : constr with_bindings -> tactic
+*)
 
+(* Equivalent to [general_rewrite l2r] *)
 val rewriteLR   : constr -> tactic
 val rewriteRL   : constr  -> tactic
 
+(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
+
+val general_rewrite_bindings_in :
+  bool -> identifier -> constr with_bindings -> tactic
+val general_rewrite_in          :
+  bool -> identifier -> constr -> tactic
+
 val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
-val general_rewrite_in : bool -> identifier -> constr with_bindings -> tactic
 val conditional_rewrite_in :
   bool -> identifier -> tactic -> constr with_bindings -> tactic
 
@@ -57,12 +67,36 @@ val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic
 val make_iterated_tuple : 
   env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
 
+(* The family cutRewriteIn expect an equality statement *)
+val cutRewriteInHyp : bool -> types -> identifier -> tactic
+val cutRewriteInConcl : bool -> constr -> tactic
+
+(* The family rewriteIn expect the proof of an equality *)
+val rewriteInHyp : bool -> constr -> identifier -> tactic
+val rewriteInConcl : bool -> constr -> tactic
+
+(* Expect the proof of an equality; fails with raw internal errors *)
+val substClause : bool -> constr -> identifier option -> tactic
+
+(*
+(* [substHypInConcl l2r id] is obsolete: use [rewriteInConcl l2r (mkVar id)] *)
 val substHypInConcl : bool -> identifier -> tactic
+
+(* [substConcl] is an obsolete synonym for [cutRewriteInConcl] *)
 val substConcl : bool -> constr -> tactic
-val substHyp : bool -> constr -> identifier -> tactic
 
+(* [substHyp] is an obsolete synonym of [cutRewriteInHyp] *)
+val substHyp : bool -> types -> identifier -> tactic
+*)
+
+(* Obsolete, use [rewriteInConcl lr (mkVar id)] in concl
+              or [rewriteInHyp lr (mkVar id) (Some hyp)] in hyp
+   (which, if they fail, raise only UserError, not PatternMatchingFailure)
+   or [substClause lr (mkVar id) None]
+   or [substClause lr (mkVar id) (Some hyp)]
 val hypSubst_LR : identifier -> clause -> tactic
 val hypSubst_RL : identifier -> clause -> tactic
+*)
 
 val discriminable : env -> evar_map -> constr -> constr -> bool
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11f2e38fe..dc2865be4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -41,6 +41,7 @@ open Genarg
 open Tacexpr
 open Decl_kinds
 open Evarutil
+open Indrec
 
 exception Bound
 
@@ -309,7 +310,7 @@ let rec intros_using = function
 
 let intros = tclREPEAT (intro_force false)
 
-let intro_erasing id = tclTHEN (thin [id]) (intro_using id)
+let intro_erasing id = tclTHEN (thin [id]) (introduction id)
 
 let intros_replacing ids gls = 
   let rec introrec = function
@@ -530,14 +531,13 @@ let cut c gl =
     | _  -> error "Not a proposition or a type"
 
 let cut_intro t = tclTHENFIRST (cut t) intro
-		    
-let cut_replacing id t = 
-  tclTHENFIRST
-    (cut t)
-    (tclORELSE
+
+let cut_replacing id t tac = 
+  tclTHENS (cut t)
+    [tclORELSE
       (intro_replacing id) 
-      (tclORELSE (intro_erasing id) 
-        (intro_using id)))
+      (tclORELSE (intro_erasing id) (intro_using id));
+     tac (refine_no_check (mkVar id)) ]
 
 let cut_in_parallel l = 
   let rec prec = function
@@ -895,7 +895,7 @@ let last_arg c = match kind_of_term c with
   | App (f,cl) ->  array_last cl
   | _ -> anomaly "last_arg"
 	
-let elimination_clause_scheme elimclause indclause allow_K gl = 
+let elimination_clause_scheme allow_K elimclause indclause gl = 
   let indmv = 
     (match kind_of_term (last_arg elimclause.templval.rebus) with
        | Meta mv -> mv
@@ -919,40 +919,30 @@ let type_clenv_binding wc (c,t) lbind =
  * matching I, lbindc are the expected terms for c arguments 
  *)
 
-let general_elim (c,lbindc) (elimc,lbindelimc) ?(allow_K=true) gl = 
+let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl =
   let ct = pf_type_of gl c in
   let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let indclause  = make_clenv_binding gl (c,t) lbindc  in
   let elimt      = pf_type_of gl elimc in
   let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in 
-  elimination_clause_scheme elimclause indclause allow_K gl
+  elimtac elimclause indclause gl
+
+let general_elim c e ?(allow_K=true) =
+  general_elim_clause (elimination_clause_scheme allow_K) c e
 
 (* Elimination tactic with bindings but using the default elimination 
  * constant associated with the type. *)
 
 let find_eliminator c gl =
-  let env = pf_env gl in
-  let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in
-  let s = elimination_sort_of_goal gl in
-    Indrec.lookup_eliminator ind s 
-(*  with Not_found -> 
-    let dir, base = repr_path (path_of_inductive env ind) in
-    let id = Indrec.make_elimination_ident base s in
-    errorlabstrm "default_elim"
-      (str "Cannot find the elimination combinator :" ++
-         pr_id id ++ spc () ++
-	 str "The elimination of the inductive definition :" ++
-         pr_id base ++ spc () ++ str "on sort " ++
-         spc () ++ print_sort (new_sort_in_family s) ++
-	 str " is probably not allowed")
-(* lookup_eliminator prints the message *) *)
-let default_elim (c,lbindc) gl = 
-  general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl
-
-let elim_in_context (c,_ as cx) elim gl =
-  match elim with
-  | Some (elimc,lbindelimc) -> general_elim cx (elimc,lbindelimc) gl
-  | None -> general_elim cx (find_eliminator c gl,NoBindings) gl 
+  let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+  Indrec.lookup_eliminator ind (elimination_sort_of_goal gl)
+
+let default_elim (c,_ as cx) gl = 
+  general_elim cx (find_eliminator c gl,NoBindings) gl
+
+let elim_in_context c = function
+  | Some elim -> general_elim c elim ~allow_K:true
+  | None -> default_elim c
 
 let elim (c,lbindc as cx) elim =
   match kind_of_term c with
@@ -985,31 +975,20 @@ let elimination_in_clause_scheme id elimclause indclause gl =
       (str "Nothing to rewrite in " ++ pr_id id);
   tclTHEN
     (tclEVARS (evars_of elimclause''.env))
-    (tclTHENS
-      (cut new_hyp_typ)
-      [ (* Try to insert the new hyp at the same place *)
-        tclORELSE (intro_replacing id)
-          (tclTHEN (clear [id]) (introduction id));
-        refine_no_check new_hyp_prf]) gl
-
-let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl = 
-  let ct = pf_type_of gl c in
-  let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
-  let indclause  = make_clenv_binding gl (c,t) lbindc  in
-  let elimt      = pf_type_of gl elimc in
-  let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in 
-  elimination_in_clause_scheme id elimclause indclause gl
+    (cut_replacing id new_hyp_typ
+      (fun x gls -> refine_no_check new_hyp_prf gls)) gl
+
+let general_elim_in id =
+  general_elim_clause (elimination_in_clause_scheme id)
 
 (* Case analysis tactics *)
 
 let general_case_analysis_in_context (c,lbindc) gl =
-  let env = pf_env gl in
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sigma    = project gl in 
   let sort     = elimination_sort_of_goal gl in
-  let case = if occur_term c (pf_concl gl) then Indrec.make_case_dep
-  else Indrec.make_case_gen in
-  let elim     = case env sigma mind sort in 
+  let case = 
+    if occur_term c (pf_concl gl) then make_case_dep else make_case_gen in
+  let elim     = pf_apply case gl mind sort in 
   general_elim (c,lbindc) (elim,NoBindings) gl
 
 let general_case_analysis (c,lbindc as cx) =
@@ -1372,7 +1351,7 @@ let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
   let indclause  = make_clenv_binding gl (c,typ) NoBindings  in
   let elimclause =
     make_clenv_binding gl (mkCast (elimc,elimt),elimt) lbindelimc in
-  elimination_clause_scheme elimclause indclause true gl
+  elimination_clause_scheme true elimclause indclause gl
 
 let make_up_names7 n ind (old_style,cname) = 
   if old_style (* = V6.3 version of Induction on hypotheses *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6d0f9024b..a6b906b34 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -166,15 +166,13 @@ val cut_and_apply         : constr -> tactic
 
 val general_elim  :
   constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic
+val general_elim_in :
+  identifier -> constr with_bindings -> constr with_bindings -> tactic
+
 val default_elim  : constr with_bindings -> tactic
 val simplest_elim : constr -> tactic
 val elim          : constr with_bindings -> constr with_bindings option -> tactic
-val general_elim_in : identifier -> constr * constr bindings ->
-                      constr * constr bindings -> tactic
-
 val simple_induct     : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
-val general_elim_in : identifier -> constr * constr bindings ->
-                      constr * constr bindings -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
   intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
@@ -236,7 +234,8 @@ val intros_transitivity         : constr -> tactic
 
 val cut                         : constr -> tactic
 val cut_intro                   : constr -> tactic
-val cut_replacing               : identifier -> constr -> tactic
+val cut_replacing               : 
+  identifier -> constr -> (tactic -> tactic) -> tactic
 val cut_in_parallel             : constr list -> tactic
 
 val assert_tac                  : bool -> name -> constr -> tactic