From ab0954eab207a70e6ad5f2991cc117608deff55b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Jun 2005 17:03:38 +0000
Subject: [PATCH] 1. interface of replace generalized to patterns 2.
 implementation commented out (for a little while)

---
 helm/ocaml/tactics/discriminationTactics.ml | 2 ++
 helm/ocaml/tactics/fourierR.ml              | 6 +++---
 helm/ocaml/tactics/primitiveTactics.ml      | 9 +++++----
 helm/ocaml/tactics/primitiveTactics.mli     | 3 ++-
 helm/ocaml/tactics/tactics.mli              | 5 ++++-
 5 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index f39ee677d..24ab511f0 100644
--- 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 724d2c647..c51d3bf0c 100644
--- 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 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
diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli
index 4d4eef849..68570d5ca 100644
--- 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 c4c1a32e4..30d670f3e 100644
--- 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
-- 
2.39.2