Cic.obj * CicUniv.universe_graph
type type_checked_obj =
- CheckedObj of (Cic.obj * CicUniv.universe_graph) (* cooked obj *)
- | UncheckedObj of Cic.obj (* uncooked obj *)
+ | CheckedObj of (Cic.obj * CicUniv.universe_graph)
+ | UncheckedObj of Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
-(*
- * I think this should be the real semantic:
- *
- * val is_type_checked:
- * ?trust:bool -> UriManager.uri -> bool
- *
- * but the old semantic is similar to get_cooked_obj, but
- * returns an unchecked object intead of a Not_found
- *)
val is_type_checked :
?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
type_checked_obj
(* The object whose uri is uri is unfreezed and won't be type-checked *)
(* again in the future (is_type_checked will return true) *)
(* *)
-(* Since the universes are not exported directly, but generated *)
-(* typecheking the library, we can't find them in the library as we *)
-(* do for the types. This means that when we commit uris during *)
-(* univ generation we can't associate the uri with the universe graph *)
-(* we find in the library, we have to calculate it and then inject it *)
-(* in the cacke. This is an orrible backdoor used by univ_maker. *)
-(* see the .ml file for some reassuring invariants *)
-(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
-val set_type_checking_info :
- ?replace_ugraph_and_univlist:
- ((CicUniv.universe_graph * CicUniv.universe list) option) ->
- UriManager.uri -> unit
+(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
+val set_type_checking_info : UriManager.uri ->
+ (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> 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 *)
(** total parsing time, only to benchmark the parser *)
val total_parsing_time: float ref
+val invalidate: unit -> unit
+
(* EOF *)