(* *)
(****************************************************************************)
-exception CircularDependency of string;;
+exception CircularDependency of string Lazy.t;;
exception Object_not_found of UriManager.uri;;
(* as the get cooked, but if not present the object is only fetched,
(* see the .ml file for some reassuring invariants *)
(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
val set_type_checking_info :
- ?replace_ugraph:(CicUniv.universe_graph option) -> UriManager.uri -> unit
+ ?replace_ugraph_and_univlist:
+ ((CicUniv.universe_graph * CicUniv.universe list) option) ->
+ UriManager.uri -> unit
(* this function is called by CicTypeChecker.typecheck_obj to add to the *)
(* environment a new well typed object that is not yet in the library *)
(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
val add_type_checked_obj :
- UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
+ UriManager.uri ->
+ (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
(** remove a type checked object
* @raise Object_not_found when given term is not in the environment
?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
Cic.obj * CicUniv.universe_graph
+(* get_cooked_obj_with_univlist ~trust uri *)
+(* returns the object if it is already type-checked or if it can be *)
+(* trusted (if [trust] = true and the trusting function accepts it) *)
+(* Otherwise it raises Not_found *)
+val get_cooked_obj_with_univlist :
+ ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
+ Cic.obj * CicUniv.universe_graph * CicUniv.universe list
+
(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
(* (de)serialization *)