ported debian stuff to ocaml 3.08

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 1726725c15370b146e42439def72b6b34c23c655..eeb6053aa2615b86a75efc5723d7193894896f3b 100644 (file)
--- 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
@@ -1058,7 +1072,7 @@ module DisambiguateCallbacks =
     interactive_user_uri_choice ~selection_mode ?ok
      ?enable_button_for_non_vars ~title ~msg
   let interactive_interpretation_choice = interactive_interpretation_choice
-  let input_or_locate_uri ~title ?id = input_or_locate_uri ~title
+  let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title
  end
 ;;
 
@@ -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