From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 12:31:24 +0000 (+0000)
Subject: 1. rewrite_* and rewrite_back_* merged into one function
X-Git-Tag: PRE_GETTER_STORAGE~94
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06ef12ecdaa09ed6e9c2b00554010e6b59f77744;p=helm.git

1. rewrite_* and rewrite_back_* merged into one function
2. signature of rewrite_* improved
3. concrete syntax for the rewrite direction fixed to ">" and "<"

NOTE: rewrite_* is still no longer working.
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 354b18ae5..7239e98e3 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -84,11 +84,8 @@ let tactic_of_ast = function
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Replace (_, pattern, with_what) ->
      Tactics.replace ~pattern ~with_what
-  | TacticAst.Rewrite (_, dir, t, pattern) ->
-      if dir = `Left then
-        EqualityTactics.rewrite_tac ~where:pattern ~term:t ()
-      else
-        EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
+  | TacticAst.Rewrite (_, direction, t, pattern) ->
+     EqualityTactics.rewrite_tac ~direction ~pattern t
   | TacticAst.Right _ -> Tactics.right
   | TacticAst.Ring _ -> Tactics.ring
   | TacticAst.Split _ -> Tactics.split
diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index 11396b8bd..c0662e78f 100644
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -102,5 +102,5 @@ qed.
 theorem le_gen_S_S_2: \forall m,n. (le (S m) (S n)) \to (le m n).
 intros.
 lapply le_gen_S_x_2 to H using H0. elim H0. elim H1. 
-lapply eq_gen_S_S to H2 using H4. rewrite left H4. assumption.
+lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption.
 qed.
diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
index 888ec5abd..f5ad10c7f 100644
--- a/helm/matita/tests/inversion.ma
+++ b/helm/matita/tests/inversion.ma
@@ -20,7 +20,7 @@ theorem test_inversion: \forall n. le n O \to n=O.
   generalize Hcut.
   apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
   (* first goal (left open) *)
-  intro. rewrite right H1.
+  intro. rewrite < H1.
   clear Hcut.
   (* second goal (closed) *)
   goal 14.
@@ -38,7 +38,7 @@ theorem test_inversion2: \forall n. le n O \to n=O.
  generalize (refl_equal nat O).
  apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  (* first goal (left open) *)
- intro. rewrite right H1.
+ intro. rewrite < H1.
  (* second goal (closed) *)
  goal 13.
  simplify. intros.
diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma
index 67da01e89..ce1e216ad 100644
--- a/helm/matita/tests/rewrite.ma
+++ b/helm/matita/tests/rewrite.ma
@@ -10,13 +10,13 @@ theorem a:
   \forall a,b:nat.
   a = b \to b + a + b + a= (\lambda j.((\lambda w.((\lambda x.x + b + w + j) a)) b)) a.
 intros.
-rewrite right H in \vdash (? ? ? ((\lambda j.((\lambda w.%) ?)) ?)).
+rewrite < H in \vdash (? ? ? ((\lambda j.((\lambda w.%) ?)) ?)).
 
-rewrite right H in \vdash (? ? % ?).
+rewrite < H in \vdash (? ? % ?).
 
 simplify in \vdash (? ? ? ((\lambda x.((\lambda y.%) ?)) ?)).
 
-rewrite right H in \vdash (? ? ? (% ?)).
+rewrite < H in \vdash (? ? ? (% ?)).
 simplify.
 reflexivity.
 qed.