- passes subst to FreshNameGenerator

- removed some old debugging prints

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index b6aa28caea1655e9569d1274188be940841580e5..7ba0650ce3c424345c42e036c8fac7686e9bf55b 100644 (file)
--- 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 *)