- ?replace_ugraph:(CicUniv.universe_graph option) -> UriManager.uri -> unit
-
-(* We need this in the Qed. *)
-val add_type_checked_term :
- UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
-
- (** remove a type checked term
- * @raise Term_not_found when given term is not in the environment
+ ?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 * CicUniv.universe list) -> unit
+
+ (** remove a type checked object
+ * @raise Object_not_found when given term is not in the environment