(* 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:(CicUniv.universe_graph option) -> UriManager.uri -> unit
-(* We need this in the Qed. *)
-val add_type_checked_term :
+(* 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
(** remove a type checked object
(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
-exception OnlyPutOfInductiveDefinitionsIsAllowed
-
-(* put_inductive_definition uri obj *)
-(* put [obj] (that must be an InductiveDefinition and show URI is [uri]) *)
-(* in the environment. *)
-(* WARNING: VERY UNSAFE. *)
-(* This function should be called only on a well-typed definition. *)
-val put_inductive_definition :
- UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
-
(* (de)serialization *)
val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
(** @return true for objects available in the library *)
val in_library: UriManager.uri -> bool
+ (** total parsing time, only to benchmark the parser *)
+val total_parsing_time: float ref
+
(* EOF *)