(******************************************************************************)
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, *)
(* 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) *)