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
| thms ->
String.concat ", "
(HExtlib.filter_map (function
- | NotationPt.NRef r -> Some (NCicPp.r2s true r)
+ | NotationPt.NRef r -> Some (NCicPp.r2s status true r)
| _ -> None)
thms)
in
let similarsymbols_tag_name = "similarsymbolos" in
let similarsymbols_tag = `NAME similarsymbols_tag_name in
let initial_statuses current baseuri =
- let status = new GrafiteTypes.status baseuri in
+ let status = new MatitaEngine.status baseuri in
(match current with
Some current ->
NCicLibrary.time_travel status;