merged cic_notation with matita: good luck!

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 51b17451e9caa1c1bbd9d964930dcd46368dd61b..efe629ac1903d8954781314b1109bdefbf34d8f2 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -322,19 +322,20 @@ class gui () =
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
         (* toolbar *)
-      let module A = TacticAst in
-      let hole = CicAst.UserInput in
-      let loc = CicAst.dummy_floc in
+      let module A = GrafiteAst in
+      let hole = CicNotationPt.UserInput in
+      let loc = Disambiguate.dummy_floc in
       let tac ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           (MatitaScript.instance ())#advance
-            ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
+            ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+            ()
       in
       let tac_w_term ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
           let buf = source_buffer in
           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
-            ("\n" ^ TacticAstPp.pp_tactic ast)
+            ("\n" ^ GrafiteAstPp.pp_tactic ast)
       in
       let tbar = self#main in
       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));