From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Jul 2007 20:12:41 +0000 (+0000)
Subject: Added ~with_cast to the change tactic.
X-Git-Tag: make_still_working~6223
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=73993c770d613df679df63d8d3d89fc37c02ae09;p=helm.git

Added ~with_cast to the change tactic.
When with_cast is true, a cast is recorded in the lambda term.
---

diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml
index 3afef8eed..9c39caa6f 100644
--- a/helm/software/components/tactics/reductionTactics.ml
+++ b/helm/software/components/tactics/reductionTactics.ml
@@ -135,7 +135,7 @@ exception NotConvertible
         reference variables that are local to the term that is going to be
         replaced. To fix this we should parse with_what in the context of the
         term(s) to be replaced. *)
-let change_tac ~pattern with_what  =
+let change_tac ?(with_cast=false) ~pattern with_what  =
  let change_tac ~pattern ~with_what (proof, goal) =
   let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
@@ -206,7 +206,19 @@ let change_tac ~pattern with_what  =
         | _ as t -> t)
       metasenv
   in
-  (curi,metasenv',_subst,pbo,pty, attrs), [metano]
+   let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in
+    if with_cast then
+     let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in
+     let (newproof,_) =
+       let irl= CicMkImplicit.identity_relocation_list_for_metavariable context'
+       in
+        ProofEngineHelpers.subst_meta_in_proof
+         proof metano
+          (Cic.Cast (Cic.Meta(metano',irl),ty')) [metano',context',ty']
+     in
+      newproof, [metano']
+    else
+     proof,[goal]
   in
     mk_tactic (change_tac ~pattern ~with_what)
 
diff --git a/helm/software/components/tactics/reductionTactics.mli b/helm/software/components/tactics/reductionTactics.mli
index 62200df69..f04e7dcac 100644
--- a/helm/software/components/tactics/reductionTactics.mli
+++ b/helm/software/components/tactics/reductionTactics.mli
@@ -35,7 +35,8 @@ val unfold_tac:
   pattern:ProofEngineTypes.lazy_pattern ->
     ProofEngineTypes.tactic
 
-val change_tac:
+val change_tac: 
+  ?with_cast:bool ->
   pattern:ProofEngineTypes.lazy_pattern ->
   Cic.lazy_term ->
     ProofEngineTypes.tactic