1. interface of replace generalized to patterns

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 2f1d7be47de43c0ef3d36e8b5bd5a7a372b56761..c5815471a67880622c20026a99a2e92f858042ec 100644 (file)
--- 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