From: Stefano Zacchiroli <zack@upsilon.cc>
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 *)