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 354b18ae54cd3156f72a4cdb9b6028c5056e6a80..7239e98e3e2e5ee6ce00b83e2cad8717e4c0a254 100644 (file)
--- 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 11396b8bdc8160327373a3c5f55037092028b575..c0662e78f9986fc3b6d59124efb9272f44aca417 100644 (file)
--- 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 888ec5abd130ae290ec3d09555a4859c0f8fbde2..f5ad10c7fc727fb33377c9150cad16926030786b 100644 (file)
--- 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 67da01e89c1cab029a85b18392fed4fdcfdb30cd..ce1e216adb4991320657c52277631bca57b1747f 100644 (file)
--- 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.