The rewrite_* set of tactics is now working again. However, as before,

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a28cdedf85ac214b3d56b854bb82ce454be9b19b..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
@@ -224,7 +221,14 @@ let generate_projections uri fields status =
  
 let eval_command status cmd =
   match cmd with
-  | TacticAst.Set (loc, name, value) -> set_option status name value
+  | TacticAst.Set (loc, name, value) -> 
+      let value = 
+        if name = "baseuri" then
+          MatitaMisc.strip_trailing_slash value
+        else
+          value
+      in
+      set_option status name value
   | TacticAst.Drop loc -> raise Drop
   | TacticAst.Qed loc ->
       let uri, metasenv, bo, ty =