New tactic rename (for now for internal usage only).

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index 2c641fd84f9ee3e48d625951bc970d35a61ed4e2..2e8aa404930f54a58f85810cd165ddaabc767c04 100644 (file)
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -154,6 +154,35 @@ let clear ~hyp =
  in
   mk_tactic (clear ~hyp)
 
+(* Warning: this tactic has no effect on the proof term.
+   It just changes the name of an hypothesis in the current sequent *)
+let rename ~from ~to_ =
+ let rename ~from ~to_ (proof, goal) =
+  let module C = Cic in
+   let curi,metasenv,pbo,pty = proof in
+    let metano,context,ty =
+     CicUtil.lookup_meta goal metasenv
+    in
+     let metasenv' =
+      List.map
+       (function
+           (m,canonical_context,ty) when m = metano ->
+             let canonical_context' =
+              List.map
+               (function
+                   Some (Cic.Name hyp,decl_or_def) when hyp = from ->
+                    Some (Cic.Name to_,decl_or_def)
+                 | item -> item
+               ) canonical_context
+             in
+              m,canonical_context',ty
+         | t -> t
+       ) metasenv
+     in
+      (curi,metasenv',pbo,pty), [goal]
+ in
+  mk_tactic (rename ~from ~to_)
+
 let set_goal n =
   ProofEngineTypes.mk_tactic
     (fun (proof, goal) ->

diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.mli b/helm/ocaml/tactics/proofEngineStructuralRules.mli
index 142b82b6812e1306a385c429e9ba044e43cb128e..91ebfecfb4ba94a682967d26f77e928edf30552d 100644 (file)
--- a/helm/ocaml/tactics/proofEngineStructuralRules.mli
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.mli
@@ -26,5 +26,9 @@
 val clearbody: hyp:string -> ProofEngineTypes.tactic
 val clear: hyp:string -> ProofEngineTypes.tactic
 
+(* Warning: this tactic has no effect on the proof term.
+   It just changes the name of an hypothesis in the current sequent *)
+val rename: from:string -> to_:string -> ProofEngineTypes.tactic
+
   (* change the current goal to those referred by the given meta number *)
 val set_goal: int -> ProofEngineTypes.tactic