Missing check implemented: the sort of each constructors should be constrained

[helm.git] / helm / software / components / cic_proof_checking / cicEnvironment.mli

diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.mli b/helm/software/components/cic_proof_checking/cicEnvironment.mli
index 55566a614493de9ae8b872a0a9347d2cf6a37073..0979d62d27599a9a42e1c209f6c1fdfcedc07b69 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicEnvironment.mli
+++ b/helm/software/components/cic_proof_checking/cicEnvironment.mli
@@ -47,18 +47,9 @@ val get_obj :
     Cic.obj * CicUniv.universe_graph
 
 type type_checked_obj =
-   CheckedObj of (Cic.obj * CicUniv.universe_graph)    (* cooked obj *)
- | UncheckedObj of Cic.obj  (* uncooked obj *)
+ | CheckedObj of (Cic.obj * CicUniv.universe_graph)    
+ | UncheckedObj of Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
 
-(*
- * I think this should be the real semantic:
- * 
- * val is_type_checked: 
- *  ?trust:bool -> UriManager.uri -> bool
- *
- *  but the old semantic is similar to get_cooked_obj, but 
- *  returns an unchecked object intead of a Not_found
- *)
 val is_type_checked : 
   ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->  
     type_checked_obj
@@ -68,18 +59,9 @@ val is_type_checked :
 (* The object whose uri is uri is unfreezed and won't be type-checked *)
 (* again in the future (is_type_checked will return true)             *)
 (*                                                                    *)
-(* Since the universes are not exported directly, but generated       *)
-(* typecheking the library, we can't find them in the library as we   *)
-(* do for the types. This means that when we commit uris during       *)
-(* univ generation we can't associate the uri with the universe graph *)
-(* 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_and_univlist:
-    ((CicUniv.universe_graph * CicUniv.universe list) option) -> 
-    UriManager.uri -> unit
+(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker       *)
+val set_type_checking_info : UriManager.uri -> 
+  (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
 
 (* 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    *)
@@ -133,4 +115,6 @@ val in_library: UriManager.uri -> bool
   (** total parsing time, only to benchmark the parser *)
 val total_parsing_time: float ref
 
+val invalidate: unit -> unit
+
 (* EOF *)