* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open ProofEngineTypes
let clearbody ~hyp =
Some (Cic.Name hyp',_) when hyp' = hyp ->
(true, None::context)
| None -> (b, None::context)
- | Some (_,Cic.Def (_,Some _)) -> assert false
| Some (n,C.Decl t)
+ | Some (n,Cic.Def (t,Some _))
| Some (n,C.Def (t,None)) ->
if b then
let _,_ =
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) ->