X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=3a9e87eea0a785e3d9c50f33f558cea2625d2842;hb=3ce27112fe93ced5f67cc6af8fc63037eba3f322;hp=22a8dd2248b7b28315a3b7b8d254f7157ae7f7fd;hpb=3f9cb46b5e167955e85b3d2544f1bed90f1a25b7;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 22a8dd224..3a9e87eea 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -340,7 +340,6 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
-        prerr_endline ("pp new obj \n"^NCicPp.ppobj obj);
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
         let index_obj =
@@ -390,6 +389,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                 if nstatus#ng_mode <> `CommandMode then
                   begin
                     (*HLog.warn "error in generating projection/eliminator";*)
+                    assert(status#ng_mode = `CommandMode);
                     status, uris
                   end
                 else