X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=4490e6586eba94ec42b11dfc3a836961536893e1;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=fe87fc4afc57e9141584a11a437cce9eaa28b3a2;hpb=562836b540a915d013225c2a00101e14207c44f6;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index fe87fc4af..4490e6586 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -75,15 +75,18 @@ val is_type_checked :
 (* we find in the library, we have to calculate it and then inject it *)
 (* in the cacke. This is an orrible backdoor used by univ_maker.      *)
 (* see the .ml file for some reassuring invariants                    *)
+(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
 val set_type_checking_info : 
   ?replace_ugraph:(CicUniv.universe_graph option) -> UriManager.uri -> unit
 
-(* We need this in the Qed. *)
-val add_type_checked_term : 
+(* this function is called by CicTypeChecker.typecheck_obj to add to the *)
+(* environment a new well typed object that is not yet in the library    *)
+(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
+val add_type_checked_obj : 
   UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
 
   (** remove a type checked object
-  * @raise Term_not_found when given term is not in the environment
+  * @raise Object_not_found when given term is not in the environment
   * @raise Failure when remove_term is invoked while type checking *)
 val remove_obj: UriManager.uri -> unit
 
@@ -97,16 +100,6 @@ val get_cooked_obj :
 
 (* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
 
-exception OnlyPutOfInductiveDefinitionsIsAllowed
-
-(* put_inductive_definition uri obj                                      *)
-(* put [obj] (that must be an InductiveDefinition and show URI is [uri]) *)
-(* in the environment.                                                   *)
-(* WARNING: VERY UNSAFE.                                                 *)
-(* This function should be called only on a well-typed definition.       *)
-val put_inductive_definition : 
-  UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
-
 (* (de)serialization *)
 val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
 val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
@@ -126,4 +119,7 @@ val list_uri: unit -> UriManager.uri list
   (** @return true for objects available in the library *)
 val in_library: UriManager.uri -> bool
 
+  (** total parsing time, only to benchmark the parser *)
+val total_parsing_time: float ref
+
 (* EOF *)