(******************************************************************************)
exception CircularDependency of string;;
+exception Term_not_found of UriManager.uri;;
(* get_obj uri *)
(* returns the cic object whose uri is uri. If the term is not just in cache, *)
(* again in the future (is_type_checked will return true) *)
val set_type_checking_info : UriManager.uri -> unit
+(* We need this in the Qed. *)
+val add_type_checked_term : UriManager.uri -> Cic.obj -> unit
+
+ (** remove a type checked term
+ * @raise Term_not_found when given term is not in the environment
+ * @raise Failure when remove_term is invoked while type checking *)
+val remove_term: UriManager.uri -> unit
+
(* get_cooked_obj ~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) *)