X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=3e5c2bf77c161b071c77f80366047b076f8422e1;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=e3def568e4bdeba80ae3b4ad147ed05eb6deaba2;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index e3def568e..3e5c2bf77 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -36,6 +36,7 @@
 (******************************************************************************)
 
 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, *)
@@ -64,6 +65,11 @@ 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) *)