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
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
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