]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaEngine.ml
first matitadep snapshot
[helm.git] / helm / matita / matitaEngine.ml
index a28cdedf85ac214b3d56b854bb82ce454be9b19b..354b18ae54cd3156f72a4cdb9b6028c5056e6a80 100644 (file)
@@ -224,7 +224,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 =