1. interface of replace generalized to patterns

2. implementation commented out (for a little while)

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index f39ee677d28e66fdeaacd42f2987a2eb24040657..24ab511f05d71c77f08e83e186b8be41f67f27d2 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -165,6 +165,7 @@ and injection1_tac ~term ~i =
                             ProofEngineTypes.apply_tactic 
                             (P.change_tac
                                ~what:new_t1'
+                               ~pattern:([],None)
                                ~with_what:
                                  (C.Appl [
                                    C.Lambda (
@@ -300,6 +301,7 @@ let discriminate'_tac ~term =
                              ~start:
                               (P.change_tac 
                                ~what:gty' 
+                               ~pattern:([],None)
                                ~with_what:
                                 (C.Appl [
                                   C.Lambda (

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 724d2c64708d4e4f0a6c2e07d6cf31e49a7224e0..c51d3bf0cf77e611690355ead5841272bbdd9960 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -1133,7 +1133,7 @@ let rec fourier (s_proof,s_goal)=
              let curi,metasenv,pbo,pty = proof in
              let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              apply_tactic 
-              (PrimitiveTactics.change_tac ~what:ty 
+              (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
                 ~with_what:(Cic.Appl [ _not; ineq])) 
               status))
            ~continuation:(Tacticals.then_ 
@@ -1178,8 +1178,8 @@ let rec fourier (s_proof,s_goal)=
                      |_ -> assert false)
                    in
                    let r = apply_tactic 
-                    (PrimitiveTactics.change_tac ~what:ty ~with_what:w1) 
-                    status in
+                   (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
+                      ~with_what:w1) status in
                    debug("fine MY_CHNGE\n");
                    r)) 
                  ~continuation:(*PORTINGTacticals.id_tac*)tac2]))

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

diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli
index 4d4eef84909c77f72c9df07397d3b0bd26a25de6..68570d5ca56100b38994498d8be424639c01940a 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.mli
+++ b/helm/ocaml/tactics/primitiveTactics.mli
@@ -57,4 +57,5 @@ val elim_intros_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
 
 val change_tac:
-  what: Cic.term -> with_what: Cic.term -> ProofEngineTypes.tactic 
+  what: Cic.term -> with_what: Cic.term -> pattern:ProofEngineTypes.pattern ->
+   ProofEngineTypes.tactic 

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index c4c1a32e43572c272d585629ab0f93149319c943..30d670f3ead8a55fc0cb1de24cef0b5a31caf4a6 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -5,7 +5,10 @@ val assumption : ProofEngineTypes.tactic
 val auto :
   ?depth:int ->
   ?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic
-val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
+val change :
+  what:Cic.term ->
+  with_what:Cic.term ->
+  pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
 val clear : hyp:string -> ProofEngineTypes.tactic
 val clearbody : hyp:string -> ProofEngineTypes.tactic
 val compare : term:Cic.term -> ProofEngineTypes.tactic