added too .moo files notation related statements

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b456bb6eb39c57f45f3b301e6590adccd275f91e..aff9144cc0cef8124fa492a9f7ea74ca7a7e4b64 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -572,7 +572,9 @@ let eval_command opts status cmd =
   | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
   | GrafiteAst.Dump _ -> assert false   (* ZACK: to be removed *)
   | GrafiteAst.Interpretation _
-  | GrafiteAst.Notation _ -> status
+  | GrafiteAst.Notation _ as stm ->
+      { status with moo_content_rev =
+        (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with