]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_proof_checking/cicEnvironment.mli
cicCooking.ml* forgot in the previous commit
[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.mli
index 22fd5d657e86a9b178acd182874d4a44fe3e0d52..c54df77e2ef2f0dec7516b326c3c17695f6ddb90 100644 (file)
@@ -53,7 +53,7 @@ type type_checked_obj =
 (* otherwise it returns (false,object) and freeze the object for    *)
 (* type-checking                                                    *)
 (* set_type_checking_info must be called to unfreeze the object     *)
-val is_type_checked : UriManager.uri -> int -> type_checked_obj
+val is_type_checked : UriManager.uri -> type_checked_obj
 
 (* set_type_checking_info uri                                         *)
 (* must be called once the type-checking of uri is finished           *)
@@ -61,9 +61,5 @@ val is_type_checked : UriManager.uri -> int -> type_checked_obj
 (* again in the future (is_type_checked will return true)             *)
 val set_type_checking_info : UriManager.uri -> unit
 
-(* get_cooked_obj uri cookingsno *)
-val get_cooked_obj : UriManager.uri -> int -> Cic.obj
-
-(* set_cooking_function cooking_function *)
-val set_cooking_function :
- (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) -> unit
+(* get_cooked_obj uri *)
+val get_cooked_obj : UriManager.uri -> Cic.obj