From 81ad82070892b2f2740111d97b2d72394f969328 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 10 Feb 2005 15:54:44 +0000 Subject: [PATCH] renaming "remove_term" -> "remove_obj" --- helm/ocaml/cic_proof_checking/cicEnvironment.ml | 2 +- helm/ocaml/cic_proof_checking/cicEnvironment.mli | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 05467185b..182f8b7d9 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -686,7 +686,7 @@ let in_library uri = true with Http_getter_types.Key_not_found _ -> false) -let remove_term = Cache.remove +let remove_obj = Cache.remove let list_uri () = Cache.list_all_cooked_uris () diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index 5c10c81a3..0a8b25c25 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -83,10 +83,10 @@ val set_type_checking_info : val add_type_checked_term : UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit - (** remove a type checked term + (** remove a type checked object * @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 +val remove_obj: UriManager.uri -> unit (* get_cooked_obj ~trust uri *) (* returns the object if it is already type-checked or if it can be *) -- 2.39.2