]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/gTopLevel.ml
moved environmentP3 in cic_textual_parser2 and reshaped interface
[helm.git] / helm / gTopLevel / gTopLevel.ml
index 76ebe6cc6f453ed657e0ac683f9f1773302eb5b7..8932d21a86eec829cc62fb0f32dd38bd4bcc7a33 100644 (file)
@@ -746,12 +746,12 @@ let edit_aliases () =
   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
   ignore
    (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
-     (DisambiguatingParser.Environment.to_string !id_to_uris)) ;
+     (DisambiguatingParser.EnvironmentP3.to_string !id_to_uris)) ;
   window#show () ;
   GtkThread.main ();
   if !chosen then
    id_to_uris :=
-    DisambiguatingParser.Environment.of_string (input#buffer#get_text ())
+    DisambiguatingParser.EnvironmentP3.of_string (input#buffer#get_text ())
 ;;
 
 let proveit () =