+(* 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
+