X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FprimitiveTactics.ml;h=bf65d1a7b2257e3c8da526e6492e410b8a1f276d;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=75f421cede4ec24c666700a69a1316d56fbdd818;hpb=4720c6af414c4a834a994fdb404fda2d0c04fc03;p=helm.git

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 75f421ced..bf65d1a7b 100644
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -477,3 +477,41 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*)
                     in
                      (newproof,
                       List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
+
+
+exception NotConvertible
+
+(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal,  *)
+(*CSC: while [what] can have a richer context (because of binders)           *)
+(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
+(*CSC: Is that evident? Is that right? Or should it be changed?              *)
+let change_tac ~what ~with_what ~status:(proof, goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  (* are_convertible works only on well-typed terms *)
+  ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ;
+  if CicReduction.are_convertible context what with_what then
+   begin
+    let replace =
+     ProofEngineReduction.replace ~equality:(==) ~what ~with_what
+    in
+    let ty' = replace ty in
+    let context' =
+     List.map
+      (function
+          Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
+        | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
+        | None -> None
+      ) context
+    in
+     let metasenv' = 
+      List.map
+       (function
+           (n,_,_) when n = metano -> (metano,context',ty')
+         | _ as t -> t
+       ) metasenv
+     in
+      (curi,metasenv',pbo,pty), [metano]
+   end
+  else
+   raise (ProofEngineTypes.Fail "Not convertible")