X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=89481b287434a12284dedd67c24e76c08acee8e5;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=19944417f048e440b7c5ac0ace0967fcef6cad7b;hpb=aa6153d8e480abfe52b00e1bc6bd48ef84c48988;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 19944417f..89481b287 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -24,6 +24,7 @@
  *)
 
 open Printf
+
 open MatitaTypes
 
 exception Drop;;
@@ -353,7 +354,7 @@ module MatitaStatus =
   let set_goals (status,_) goals = status,goals
 
   let id_tac status =
-    apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status
+    apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) status
 
   let mk_tactic tac = tac
 
@@ -451,21 +452,18 @@ let eval_coercion status coercion =
    List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
     status new_coercions in
   let statement_of name =
-    GrafiteAstPp.pp_statement 
-      (GrafiteAst.Executable (Disambiguate.dummy_floc,
-        (GrafiteAst.Command (Disambiguate.dummy_floc,
-          (GrafiteAst.Coercion (Disambiguate.dummy_floc, 
-            (CicNotationPt.Ident (name, None)))))))) ^ "\n"
+    GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, 
+      (CicNotationPt.Ident (name, None)))
   in
-  let moo_content_rev =
-    [statement_of (UriManager.name_of_uri coer_uri)] @ 
+  let moo_content = 
+    statement_of (UriManager.name_of_uri coer_uri) ::
     (List.map 
       (fun (uri, _, _) -> 
         statement_of (UriManager.name_of_uri uri))
-    new_coercions) @ status.moo_content_rev 
+    new_coercions)
   in
-  let status =  {status with moo_content_rev = moo_content_rev} in
-  {status with proof_status = No_proof}
+  let status = add_moo_content moo_content status in
+  { status with proof_status = No_proof }
 
 let generate_elimination_principles uri status =
  let elim sort status =
@@ -571,8 +569,7 @@ let eval_command opts status cmd =
   match cmd with
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
-     {status with moo_content_rev =
-        (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
+     add_moo_content [cmd] status
   | GrafiteAst.Include (loc, path) ->
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = MatitaMisc.obj_file_of_script absolute_path in
@@ -649,11 +646,7 @@ let eval_command opts status cmd =
   | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
   | GrafiteAst.Dump _ -> assert false   (* ZACK: to be removed *)
   | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
-      let status' =
-        { status with
-            moo_content_rev =
-              (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
-      in
+      let status' = add_moo_content [stm] status in
       let aliases' =
         DisambiguateTypes.Environment.cons
           (DisambiguateTypes.Symbol (symbol, 0))
@@ -661,9 +654,7 @@ let eval_command opts status cmd =
           status.aliases
       in
       MatitaSync.set_proof_aliases status' aliases'
-  | GrafiteAst.Notation _ as stm ->
-      { status with moo_content_rev =
-        (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
+  | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with