From: Stefano Zacchiroli Date: Mon, 29 Nov 2004 12:30:31 +0000 (+0000) Subject: - passes subst to FreshNameGenerator X-Git-Tag: PRE_UNIVERSES~3 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a482ae2ca1849bfe49b057411b6d0af98440e9c0;p=helm.git - passes subst to FreshNameGenerator - removed some old debugging prints --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index b6aa28cae..7ba0650ce 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -444,7 +444,6 @@ let qed () = (*let old_working = CicUniv.get_working () in CicUniv.set_working (CicUniv.get_global ());*) CicUniv.directly_to_env_begin () ; - prerr_endline "-------------> QED"; if CicReduction.are_convertible [] (CicTypeChecker.type_of_aux' [] [] bo) ty @@ -469,7 +468,6 @@ let qed () = CicUniv.qed (); (* now the env has the right constraints *)*) CicUniv.directly_to_env_end(); CicUniv.reset_working (); - prerr_endline "-------------> FINE"; end else raise WrongProof @@ -522,7 +520,7 @@ let decompose_uris_choice_callback uris = let mk_fresh_name_callback metasenv context name ~typ = let fresh_name = - match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with + match FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ with Cic.Name fresh_name -> fresh_name | Cic.Anonymous -> assert false in @@ -607,10 +605,7 @@ let refresh_goals ?(empty_notebook=true) notebook = begin notebook#set_current_page ~may_skip_switch_page_event:true metano ; -prerr_endline "CIAO CIAO" ; -prerr_endline ("SEQUENTE CORRENTE: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; notebook#proofw#load_sequent metasenv currentsequent ; -prerr_endline "pASSO CIAO CIAO" end with e -> @@ -2829,16 +2824,13 @@ end (* MAIN *) let initialize_everything () = -prerr_endline "STO PER CREARE LA PROOF WINDOW" ; let output = TermViewer.proof_viewer ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object ~width:350 ~height:280 () in -prerr_endline "CREATA" ; let notebook = new notebook in let rendering_window' = new rendering_window output notebook in -prerr_endline "OK" ; rendering_window'#set_auto_disambiguation !auto_disambiguation; set_rendering_window rendering_window'; let print_error_as_html prefix msg = @@ -2856,7 +2848,6 @@ prerr_endline "OK" ; ;; let main () = -prerr_endline "CIAO" ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; MQIC.close mqi_handle; @@ -2864,6 +2855,7 @@ prerr_endline "CIAO" ; ;; try +(* CicEnvironment.set_trust (fun _ -> false); *) Sys.catch_break true; main (); with Sys.Break -> () (* exit nicely, invoking at_exit functions *)