]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/matitaScript.ml
Interface reduction; code clean up.
[helm.git] / matita / matita / matitaScript.ml
index 37e0f92395351c662d8031477b57ae8aadd191e3..f1b20efe5929eff2ca0cde49d2e4edf8efc01789 100644 (file)
@@ -125,7 +125,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
-      MatitaMathView.show_entry (`NCic (t,ctx,m,s));
+      MatitaMathView.cicBrowser (Some (`NCic (t,ctx,m,s)));
       [status, parsed_text], "", parsed_text_length
   | TA.NIntroGuess _loc ->
       let names_ref = ref [] in