X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=eeb6053aa2615b86a75efc5723d7193894896f3b;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=bda4c4b826126a2caf354bfdd5e7838227e6f8d6;hpb=978a25d9392e5fc1a19fa37c86339c5d0b67ddd6;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index bda4c4b82..eeb6053aa 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -469,6 +469,11 @@ let qed () =
     None -> assert false
   | Some (uri,[],bo,ty) ->
      let uri = match uri with Some uri -> uri | _ -> assert false in
+     (* we want to typecheck in the ENV *)
+     (*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
@@ -484,7 +489,16 @@ let qed () =
         let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
          make_dirs pathname ;
          save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
-          pathname
+          pathname;
+	(* add the object to the env *)
+	CicEnvironment.add_type_checked_term uri (
+	 Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+	(* FIXME: the variable list!! *)
+	(*
+	CicUniv.qed (); (* now the env has the right constraints *)*)
+	CicUniv.directly_to_env_end();
+	CicUniv.reset_working ();
+     prerr_endline "-------------> FINE";
       end
      else
       raise WrongProof
@@ -1593,7 +1607,8 @@ let open_ () =
  let notebook = (rendering_window ())#notebook in
    try
     let uri = input_or_locate_uri ~title:"Open" in
-     CicTypeChecker.typecheck uri ;
+     ignore(CicTypeChecker.typecheck uri);
+     (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
      let metasenv,bo,ty =
       match CicEnvironment.get_cooked_obj uri with
          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty