X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=c5815471a67880622c20026a99a2e92f858042ec;hb=7b78ae643999aa95b95b376fab54adb33dbed206;hp=2f1d7be47de43c0ef3d36e8b5bd5a7a372b56761;hpb=abd9e5cfa8e7b6923e0664a4813a0a842f5c4e76;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 2f1d7be47..c5815471a 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -595,8 +595,9 @@ exception NotConvertible
 (*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 =
-  let change_tac ~what ~with_what (proof, goal) =
+let change_tac ~what ~with_what ~pattern =
+(*
+  let change_tac ~what ~with_what ~pattern (proof, goal) =
     let curi,metasenv,pbo,pty = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
       (* are_convertible works only on well-typed terms *)
@@ -636,5 +637,5 @@ let change_tac ~what ~with_what =
       else
 	raise (ProofEngineTypes.Fail "Not convertible")
   in
-    mk_tactic (change_tac ~what ~with_what)
-      
+    mk_tactic (change_tac ~what ~with_what ~pattern)
+*) assert false