Ajout tactiques Rename et Pose; modifications pour Inversion

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

15 files changed, 179 insertions, 89 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4d0a80bdd7..5c11995503 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -317,11 +317,18 @@ GEXTEND Gram
             | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var c
             | _ -> assert false in
 	  <:ast< (TrueCut $t $id) >>
-      | IDENT "Assert"; c = constrarg; ":="; t = constrarg ->
+      | IDENT "Assert"; c = constrarg; ":="; b = constrarg ->
           let id = match c with 
             | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var c
             | _ -> assert false in
-	  <:ast< (Forward $t $id) >>
+	  <:ast< (Forward "HideBody" $b $id) >>
+      | IDENT "Pose"; c = constrarg; ":="; b = constrarg ->
+          let id = match c with 
+            | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var c
+            | _ -> assert false in 
+	  <:ast< (Forward "KeepBody" $b $id) >>
+      | IDENT "Pose"; b = constrarg ->
+	  <:ast< (Forward "KeepBody" $b) >>
       | IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list ->
           <:ast< (Specialize $n ($LIST $lcb))>>
       | IDENT "Specialize"; lcb = constrarg_binding_list ->
@@ -339,6 +346,8 @@ GEXTEND Gram
                 <:ast< (ClearBody (CLAUSE ($LIST $l))) >>
       | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> 
                 <:ast< (MoveDep $id1 $id2) >>
+      | IDENT "Rename"; id1 = identarg; IDENT "into"; id2 = identarg -> 
+                <:ast< (Rename $id1 $id2) >>
 (*To do: put Abstract in Refiner*)
       | IDENT "Abstract"; tc = tactic_expr -> <:ast< (ABSTRACT (TACTIC $tc)) >>
       | IDENT "Abstract"; tc = tactic_expr; "using";  s=identarg ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ea524791a4..c6057367e8 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -235,19 +235,22 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
   else 
     List.rev_append left (moverec [] [declfrom] right)
 
+(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
+   returns [tail::(f head (id,_,_) tail)] *)
 let apply_to_hyp sign id f =
   let found = ref false in
   let sign' =
     fold_named_context_both_sides
-      (fun sign (idc,c,ct as d) tail ->
+      (fun head (idc,c,ct as d) tail ->
 	 if idc = id then begin
-	   found := true; f sign d tail
+	   found := true; f head d tail
 	 end else 
-	   add_named_decl d sign)
+	   add_named_decl d head)
       sign ~init:empty_named_context
   in
   if (not !check) || !found then sign' else error "No such assumption"
 
+(* Same but with whole environment *)
 let apply_to_hyp2 env id f =
   let found = ref false in
   let env' =
@@ -261,6 +264,20 @@ let apply_to_hyp2 env id f =
   in
   if (not !check) || !found then env' else error "No such assumption"
 
+exception Found of int
+
+let apply_to_hyp_and_dependent_on sign id f g =
+  let found = ref false in
+  let sign =
+    Sign.fold_named_context
+      (fun (idc,_,_ as d) oldest ->
+         if idc = id then (found := true; add_named_decl (f d) oldest)
+         else if !found then add_named_decl (g d) oldest
+         else add_named_decl d oldest)
+      sign ~init:empty_named_context
+  in
+  if (not !check) || !found then sign else error "No such assumption"
+
 let global_vars_set_of_var = function
   | (_,None,t) -> global_vars_set (Global.env()) (body_of_type t)
   | (_,Some c,t) ->
@@ -280,7 +297,7 @@ let check_forward_dependencies id tail =
   List.iter
     (function (id',_,_ as decl) ->
        if occur_var_in_decl env id decl then
-	 error ((string_of_id id) ^ " is used in the hypothesis " 
+	 error ((string_of_id id) ^ " is used in hypothesis " 
 		^ (string_of_id id')))
     tail
 
@@ -316,6 +333,12 @@ let convert_def inbody sign sigma id c =
 		  (b,c)) in
 	     add_named_decl (idc,Some b,t) sign)
 
+
+let rename_hyp id1 id2 sign =
+  apply_to_hyp_and_dependent_on sign id1
+    (fun (_,b,t) -> (id2,b,t))
+    (map_named_declaration (replace_vars [id1,mkVar id2]))
+
 let replace_hyp sign id d =
   apply_to_hyp sign id
     (fun sign _ tail ->
@@ -559,9 +582,21 @@ let prim_refiner r sigma goal =
   	let hyps' = 
 	  move_after withdep toleft (left,declfrom,right) hto in
   	[mk_goal hyps' cl]
-	
+
+    | { name = Rename; hypspecs = [id1]; newids = [id2] } ->
+        if id1 <> id2 & List.mem id2 (ids_of_named_context sign) then
+          error ((string_of_id id2)^" is already used");
+        let sign' = rename_hyp id1 id2 sign in
+        let cl' = replace_vars [id1,mkVar id2] cl in
+        [mk_goal sign' cl']
+
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
+(* Util *)
+let rec rebind id1 id2 = function
+  | [] -> []
+  | id::l -> if id = id1 then id2::l else id::(rebind id1 id2 l)
+
 let prim_extractor subfun vl pft =
   let cl = pft.goal.evar_concl in
   match pft with
@@ -653,7 +688,10 @@ let prim_extractor subfun vl pft =
 	
     | {ref=Some(Prim{name=Move _;hypspecs=ids},[pf])} ->
 	subfun vl pf
-	  
+
+    | {ref=Some(Prim{name=Rename;hypspecs=[id1];newids=[id2];},[pf])} ->
+	subfun (rebind id1 id2 vl) pf
+
     | {ref=Some(Prim _,_)} ->
 	error "prim_extractor handed unrecognizable primitive proof"
 	  
@@ -729,5 +767,8 @@ let pr_prim_rule = function
   | {name=Move withdep;hypspecs=[id1;id2]} ->
       (str (if withdep then "Dependent " else "") ++
 	 str"Move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+  | {name=Rename;hypspecs=[id1];newids=[id2]} ->
+      (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
       
   | _ -> anomaly "pr_prim_rule: Unrecognized primitive rule"
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 9965488c9f..f1df084b2b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -46,6 +46,7 @@ type prim_rule_name =
   | Thin
   | ThinBody
   | Move of bool
+  | Rename
 
 type prim_rule = {
   name : prim_rule_name;
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index aab94e4b46..dd6f0f05d9 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -49,6 +49,7 @@ type prim_rule_name =
   | Thin
   | ThinBody
   | Move of bool
+  | Rename
 
 type prim_rule = {
   name : prim_rule_name;
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index adb4df3d53..362bac2a60 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -260,6 +260,11 @@ let move_hyp with_dep id1 id2 gl =
                   hypspecs = [id1;id2]; terms = [];
 		  newids = []; params = []}) gl
 
+let rename_hyp id1 id2 gl = 
+  refiner (Prim { name = Rename;
+                  hypspecs = [id1]; terms = [];
+		  newids = [id2]; params = []}) gl
+
 let mutual_fix lf ln lar pf = 
   refiner (Prim { name = FixRule; newids = lf;
                   hypspecs = []; terms = lar;
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d520d200db..eba872a772 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -163,6 +163,7 @@ val convert_defbody : identifier -> constr -> tactic
 val thin            : identifier list -> tactic
 val thin_body       : identifier list -> tactic
 val move_hyp        : bool -> identifier -> identifier -> tactic
+val rename_hyp      : identifier -> identifier -> tactic
 val mutual_fix      : identifier list -> int list -> constr list -> tactic
 val mutual_cofix    : identifier list -> constr list -> tactic
 val rename_bound_var_goal : tactic
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index a149b0f070..517c522f4e 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -259,7 +259,9 @@ Syntax tactic
   | cut [<<(Cut $C)>>] -> ["Cut " $C]
   | truecutid [<<(TrueCut $C $id)>>] -> ["Assert " $id " : " $C]
   | truecut [<<(TrueCut $C)>>] -> ["Assert " $C]
-  | forward [<<(Forward $C $id)>>] -> ["Assert " $id " := " $C]
+  | forward [<<(Forward _ $C $id)>>] -> ["Assert " $id " := " $C]
+  | pose_named [<<(Forward "KeepBody" $C $id)>>] -> ["Pose " $id " := " $C]
+  | pose_anon  [<<(Forward "KeepBody" $C)>>] -> ["Pose " $C]
 
   | lettac_cons [<<(LetTac $id $c (LETPATTERNS $p ($LIST $pl)))>>] -> 
 	["LetTac" [1 1] $id ":=" $c [1 1] "in" [1 1] (LETPATTERNS $p ($LIST $pl))]
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 15ca016330..6e6de2f3b7 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -72,7 +72,8 @@ and general_decompose recognizer id =
     (introElimAssumsThen
        (fun bas ->
 	  tclTHEN (clear_one id)
-	    (tclMAP (general_decompose_on_hyp recognizer) bas.assums)))
+	    (tclMAP (general_decompose_on_hyp recognizer)
+               (ids_of_named_context bas.assums))))
     id
 
 (* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste
@@ -163,18 +164,19 @@ let induction_trailer abs_i abs_j bargs =
        (fun id gls ->
 	  let idty = pf_type_of gls (mkVar id) in
 	  let fvty = global_vars (pf_env gls) idty in
-	  let possible_bring_ids =
-	    (List.tl (nLastHyps (abs_j - abs_i) gls))
-            @bargs.assums in
-	  let (ids,_) = List.fold_left 
-			  (fun (bring_ids,leave_ids) cid ->
-                             let cidty = pf_type_of gls (mkVar cid) in
-                             if not (List.mem cid leave_ids)
-                             then (cid::bring_ids,leave_ids)
-                             else (bring_ids,cid::leave_ids))
-			  ([],fvty) possible_bring_ids 
-	  in 
-	  (tclTHEN (tclTHEN (bring_hyps ids) (clear_clauses (List.rev ids)))
+	  let possible_bring_hyps =
+	    (List.tl (nLastHyps (abs_j - abs_i) gls)) @ bargs.assums
+          in
+	  let (hyps,_) =
+            List.fold_left 
+	      (fun (bring_ids,leave_ids) (cid,_,cidty as d) ->
+                 if not (List.mem cid leave_ids)
+                 then (d::bring_ids,leave_ids)
+                 else (bring_ids,cid::leave_ids))
+	      ([],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))
 
 let double_ind abs_i abs_j gls =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 68b2ca4ab5..2a37b3b19b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -189,10 +189,9 @@ let introsReplacing = intros_replacing (* déplacé *)
 let rec dependent_hyps id idlist sign = 
   let rec dep_rec =function
     | [] -> []
-    | (id1::l) -> 
-	let (_,_,id1ty) = lookup_named id1 sign in  
+    | (id1,_,id1ty as d1)::l -> 
 	if occur_var (Global.env()) id (body_of_type id1ty)
-        then id1::dep_rec l
+        then d1 :: dep_rec l
         else dep_rec l
   in 
   dep_rec idlist 
@@ -201,7 +200,7 @@ let generalizeRewriteIntros tac depids id gls =
   let dids = dependent_hyps id depids (pf_env gls) in
   (tclTHEN (bring_hyps dids)
      (tclTHEN tac
-	(introsReplacing dids)))
+	(introsReplacing (ids_of_named_context dids))))
   gls
 
 let var_occurs_in_pf gl id =
@@ -209,11 +208,28 @@ let var_occurs_in_pf gl id =
   occur_var env id (pf_concl gl) or
   List.exists (occur_var_in_decl env id) (pf_hyps gl)
 
-let split_dep_and_nodep idl gl =
+let split_dep_and_nodep hyps gl =
   List.fold_right 
-    (fun id (l1,l2) ->
-       if var_occurs_in_pf gl id then (id::l1,l2) else (l1,id::l2))
-    idl ([],[])
+    (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
@@ -280,18 +296,20 @@ let case_trailer_gene othin neqns ba gl =
                               tclTRY (projectAndApply thin id depids)))))
 		  (tclTHEN
                      (onHyps (compose List.rev (afterHyp last)) bring_hyps)
-                     (onHyps (afterHyp last) clear))))
+                     (onHyps (afterHyp last)
+                        (compose clear ids_of_named_context)))))
       | None -> tclIDTAC
   in
   (tclTHEN (tclDO neqns intro)
      (tclTHEN (bring_hyps nodepids)
-	(tclTHEN (clear_clauses nodepids)
+	(tclTHEN (clear_clauses (ids_of_named_context nodepids))
 	   (tclTHEN (onHyps (compose List.rev (nLastHyps neqns)) bring_hyps)
-	      (tclTHEN (onHyps (nLastHyps neqns) clear_clauses)
+	      (tclTHEN (onHyps (nLastHyps neqns)
+                          (compose clear_clauses ids_of_named_context))
 		 (tclTHEN rewrite_eqns
-		    (tclMAP (fun id ->
+		    (tclMAP (fun (id,_,_ as d) ->
 			       (tclORELSE (clear_clause id)
-				  (tclTHEN (bring_hyps [id])
+				  (tclTHEN (bring_hyps [d])
 				     (clear_one id))))
 		       depids)))))))
   gl
@@ -307,7 +325,8 @@ let case_trailer othin neqns ba gl =
     match othin with
       | Some thin ->
           (tclTHEN (onHyps (compose List.rev (nLastHyps neqns)) bring_hyps)
-             (tclTHEN (onHyps (nLastHyps neqns) clear_clauses)
+             (tclTHEN (onHyps (nLastHyps neqns) 
+                         (compose clear_clauses ids_of_named_context))
 		(tclTHEN
 		   (tclDO neqns
                       (tclTHEN intro
@@ -315,13 +334,13 @@ let case_trailer othin neqns ba gl =
 			    (fun id -> 
 			       tclTRY (projectAndApply thin id depids)))))
 		   (tclTHEN (tclDO (List.length nodepids) intro)
-		      (tclMAP (fun id -> 
+		      (tclMAP (fun (id,_,_) -> 
 				 tclTRY (clear_clause id)) depids)))))
       | None -> tclIDTAC
   in
   (tclTHEN (tclDO neqns intro)
      (tclTHEN (bring_hyps nodepids)
-	(tclTHEN (clear_clauses nodepids)
+	(tclTHEN (clear_clauses (ids_of_named_context nodepids))
 	   rewrite_eqns)))
   gl
 
@@ -379,7 +398,7 @@ let res_case_then gene thin indbinding id status gl =
                  (applist(mkVar id,
                           list_tabulate
                             (fun _ -> mkMeta(Clenv.new_meta())) neqns)))
-              Auto.default_auto))])
+              reflexivity))])
   gl
 
 (* Error messages of the inversion tactics *)
@@ -494,18 +513,19 @@ let (half_dinv_with, dinv_with, dinv_clear_with) =
  * back to their places in the hyp-list. *)
 
 let invIn com id ids gls =
+  let hyps = List.map (pf_get_hyp gls) ids in
   let nb_prod_init = nb_prod (pf_concl gls) in
   let intros_replace_ids gls =
     let nb_of_new_hyp =
-      nb_prod (pf_concl gls) - (List.length ids + nb_prod_init)
+      nb_prod (pf_concl gls) - (List.length hyps + nb_prod_init)
     in 
     if nb_of_new_hyp < 1 then 
       introsReplacing ids gls
     else 
-      (tclTHEN (tclDO nb_of_new_hyp intro) (introsReplacing ids)) gls
+      tclTHEN (tclDO nb_of_new_hyp intro) (introsReplacing ids) gls
   in
   try 
-    (tclTHEN (bring_hyps ids)
+    (tclTHEN (bring_hyps hyps)
        (tclTHEN (inv false com NoDep id)
           (intros_replace_ids)))
     gls
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index bc3e8ca561..a4ed4f6c58 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -372,6 +372,7 @@ let useInversionLemma =
   fun id c -> gentac [Identifier id;Constr c]
 
 let lemInvIn id c ids gls =
+  let hyps = List.map (pf_get_hyp gls) ids in
   let intros_replace_ids gls =
     let nb_of_new_hyp  = nb_prod (pf_concl gls) - List.length ids in 
     if nb_of_new_hyp < 1  then 
@@ -380,7 +381,7 @@ let lemInvIn id c ids gls =
       (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)) gls
   in 
 (*  try *)
-    ((tclTHEN (tclTHEN (bring_hyps ids) (lemInv id c))
+    ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
         (intros_replace_ids)) gls)
 (*  with Not_found -> errorlabstrm "LemInvIn" (not_found_message ids)
     |  UserError(a,b) -> errorlabstrm "LemInvIn" b  
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index d7397e8fcb..4675f9c8a3 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -33,6 +33,7 @@ let v_clear         = hide_tactic "Clear"         dyn_clear
 let v_clear_body    = hide_tactic "ClearBody"     dyn_clear_body
 let v_move          = hide_tactic "Move"          dyn_move
 let v_move_dep      = hide_tactic "MoveDep"       dyn_move_dep
+let v_rename        = hide_tactic "Rename"        dyn_rename
 let v_apply         = hide_tactic "Apply"         dyn_apply
 let v_cutAndResolve = hide_tactic "CutAndApply"   dyn_cut_and_apply
 let v_cut           = hide_tactic "Cut"           dyn_cut
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index b7b2767010..d7b1eddbc3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -153,7 +153,7 @@ let allHyps gl = pf_ids_of_hyps gl
    after id *)
 
 let afterHyp id gl =
-  fst (list_splitby (fun hyp -> hyp = id) (pf_ids_of_hyps gl))
+  fst (list_splitby (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
     
 
 (* Create a singleton clause list with the last hypothesis from then context *)
@@ -164,7 +164,7 @@ let lastHyp gl = List.hd (pf_ids_of_hyps gl)
 (* Create a clause list with the n last hypothesis from then context *)
 
 let nLastHyps n gl =
-  try list_firstn n (pf_ids_of_hyps gl)
+  try list_firstn n (pf_hyps gl)
   with Failure "firstn" -> error "Not enough hypotheses in the goal"
 
 
@@ -249,7 +249,7 @@ type branch_args = {
 
 type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
-  assums    : identifier list; (* the list of assumptions introduced *)
+  assums    : named_context; (* the list of assumptions introduced *)
   cargs     : identifier list; (* the constructor arguments *)
   constargs : identifier list; (* the CONSTANT constructor arguments *)
   recargs   : identifier list; (* the RECURSIVE constructor arguments *)
@@ -386,22 +386,22 @@ let make_elim_branch_assumptions ba gl =
             constargs = constargs;
             recargs   = recargs;
             indargs   = indargs}
-      | ((true::tl), (recarg::indarg::idtl)) ->
+      | ((true::tl), ((idrec,_,_ as recarg)::(idind,_,_ as indarg)::idtl)) ->
 	  makerec (recarg::indarg::assums,
-		   recarg::cargs,
-		   recarg::recargs,
+		   idrec::cargs,
+		   idrec::recargs,
 		   constargs,
-		   indarg::indargs) tl idtl
-      | ((false::tl), (constarg::idtl))      ->
+		   idind::indargs) tl idtl
+      | ((false::tl), ((id,_,_ as constarg)::idtl))      ->
 	  makerec (constarg::assums,
-		   constarg::cargs,
-		   constarg::constargs,
+		   id::cargs,
+		   id::constargs,
 		   recargs,
 		   indargs) tl idtl
       | (_, _) -> error "make_elim_branch_assumptions"
   in 
   makerec ([],[],[],[],[]) ba.branchsign
-    (try list_firstn ba.nassums (pf_ids_of_hyps gl)
+    (try list_firstn ba.nassums (pf_hyps gl)
      with Failure _ -> anomaly "make_elim_branch_assumptions")
 
 let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
@@ -416,20 +416,20 @@ let make_case_branch_assumptions ba gl =
             constargs = constargs;
             recargs   = recargs;
             indargs   = []}
-      | ((true::tl), (recarg::idtl)) ->
+      | ((true::tl), ((idrec,_,_ as recarg)::idtl)) ->
 	  makerec (recarg::assums,
-		   recarg::cargs,
-		   recarg::recargs,
+		   idrec::cargs,
+		   idrec::recargs,
 		   constargs) tl idtl
-      | ((false::tl), (constarg::idtl)) ->
+      | ((false::tl), ((id,_,_ as constarg)::idtl)) ->
 	  makerec (constarg::assums,
-		   constarg::cargs,
+		   id::cargs,
 		   recargs,
-		   constarg::constargs) tl idtl
+		   id::constargs) tl idtl
       | (_, _) -> error "make_case_branch_assumptions"
   in 
   makerec ([],[],[],[]) ba.branchsign
-    (try list_firstn ba.nassums (pf_ids_of_hyps gl)
+    (try list_firstn ba.nassums (pf_hyps gl)
      with Failure _ -> anomaly "make_case_branch_assumptions")
 
 let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index bb3aa3761d..a984d791f9 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -65,9 +65,9 @@ val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
 val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
 val allHyps    : goal sigma -> identifier list
-val afterHyp   : identifier -> goal sigma -> identifier list
+val afterHyp   : identifier -> goal sigma -> named_context
 val lastHyp    : goal sigma -> identifier
-val nLastHyps  : int -> goal sigma -> identifier list
+val nLastHyps  : int -> goal sigma -> named_context
 
 val allClauses : goal sigma -> clause list
 
@@ -87,10 +87,10 @@ val ifOnHyp        :
   (identifier * types -> bool) ->
     (identifier -> tactic) -> (identifier -> tactic) -> identifier -> tactic
 
-val onHyps         : (goal sigma -> identifier list) -> 
-                     (identifier list -> tactic) -> tactic
+val onHyps         : (goal sigma -> named_context) -> 
+                     (named_context -> tactic) -> tactic
 val tryAllHyps     : (identifier -> tactic) -> tactic
-val onNLastHyps    : int -> (identifier -> tactic) -> tactic
+val onNLastHyps    : int -> (named_declaration -> tactic) -> tactic
 val onLastHyp      : (identifier -> tactic) -> tactic
 
 (* [ConclPattern concl pat tacast]:
@@ -113,7 +113,7 @@ type branch_args = {
 
 type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
-  assums    : identifier list; (* the list of assumptions introduced *)
+  assums    : named_context;   (* the list of assumptions introduced *)
   cargs     : identifier list; (* the constructor arguments *)
   constargs : identifier list; (* the CONSTANT constructor arguments *)
   recargs   : identifier list; (* the RECURSIVE constructor arguments *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ef430f9b64..80dad1b6bf 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -101,7 +101,8 @@ let convert_concl   = Tacmach.convert_concl
 let convert_hyp     = Tacmach.convert_hyp
 let thin            = Tacmach.thin 
 let thin_body       = Tacmach.thin_body 
-let move_hyp        = Tacmach.move_hyp 
+let move_hyp        = Tacmach.move_hyp
+let rename_hyp      = Tacmach.rename_hyp
 
 let mutual_fix   = Tacmach.mutual_fix
 let fix f n      = mutual_fix [f] [n] []
@@ -497,13 +498,10 @@ let apply_type hdcty argl gl =
 let apply_term hdc argl gl =
   refine (applist (hdc,argl)) gl
 
-let bring_hyps ids gl = 
-  let newcl = 
-    List.fold_right 
-      (fun id cl' -> mkNamedProd id (pf_type_of gl (mkVar id)) cl')
-      ids (pf_concl gl)
-  in 
-  apply_type newcl (List.map mkVar ids) gl
+let bring_hyps hyps gl = 
+  let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
+  let f = mkCast (mkMeta (new_meta()),newcl) in
+  refine (mkApp (f, instance_from_named_context hyps)) gl
 
 (* Resolution with missing arguments *)
 
@@ -776,14 +774,8 @@ let letin_tac with_eq name c occs gl =
       depdecls in
   let t = pf_type_of gl c in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
-  let args = List.map (fun (id,_,_) -> mkVar id) depdecls in
+  let args = Array.to_list (instance_from_named_context depdecls) in
   let newcl = mkNamedLetIn id c t tmpcl in
-(*
-    if with_eq then
-    else (* To fix : add c to args, or use LetIn and clear the body *)
-      mkNamed id t tmpcl
-  in
-*)
   let lastlhyp = if marks=[] then None else snd (List.hd marks) in
   tclTHENLIST
     [ apply_type newcl args;
@@ -812,11 +804,17 @@ let dyn_lettac args gl = match args with
       letin_tac true (Name id) c (o,l) gl
   | l -> bad_tactic_args "letin" l
 
+let nowhere = (Some [],[])
+
 let dyn_forward args gl = match args with
-  | [Command com; Identifier id] ->
-      letin_tac false (Name id) (pf_interp_constr gl com) (None,[]) gl
-  | [Constr c; Identifier id]    ->
-      letin_tac false (Name id) c (None,[]) gl
+  | [Quoted_string s; Command com; Identifier id] ->
+      letin_tac (s="KeepBody") (Name id) (pf_interp_constr gl com) nowhere gl
+  | [Quoted_string s; Constr c; Identifier id]    ->
+      letin_tac (s="KeepBody") (Name id) c nowhere gl
+  | [Quoted_string s; Constr c] ->
+      letin_tac (s="KeepBody") Anonymous c nowhere gl
+  | [Quoted_string s; Command c] ->
+      letin_tac (s="KeepBody") Anonymous (pf_interp_constr gl c) nowhere gl
   | l -> bad_tactic_args "forward" l
 
 (********************************************************************)
@@ -955,11 +953,17 @@ let dyn_new_hyp argsl gl =
 
 let dyn_move = function
   | [Identifier idfrom; Identifier idto] -> move_hyp false idfrom idto
-  | _ -> assert false
+  | l -> bad_tactic_args "move" l 
 
 let dyn_move_dep = function
   | [Identifier idfrom; Identifier idto] -> move_hyp true idfrom idto
-  | _ -> assert false
+  | l -> bad_tactic_args "move_dep" l 
+
+(* Renaming hypotheses *)
+
+let dyn_rename = function
+  | [Identifier idfrom; Identifier idto] -> rename_hyp idfrom idto
+  | l -> bad_tactic_args "rename" l 
 
 (************************)
 (* Introduction tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 2df23a30fb..568ce9c484 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -167,11 +167,13 @@ val dyn_new_hyp   : tactic_arg list -> tactic
 val dyn_move      : tactic_arg list -> tactic
 val dyn_move_dep  : tactic_arg list -> tactic
 
+val dyn_rename    : tactic_arg list -> tactic
+
 (*s Resolution tactics. *)
 
 val apply_type : constr -> constr list -> tactic
 val apply_term : constr -> constr list -> tactic
-val bring_hyps : identifier list -> tactic
+val bring_hyps : named_context -> tactic
 
 val apply                 : constr      -> tactic
 val apply_without_reduce  : constr      -> tactic