Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 20 deletions

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 9c4d62b95c..9f2bde9b88 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -13,29 +13,26 @@ open Environ
 
 (* Basic operations of the typing machine. *)
 
-val make_judge : constr -> typed_type -> unsafe_judgment
+val make_judge : constr -> types -> unsafe_judgment
 
-val j_val_only : unsafe_judgment -> constr
+val j_val : unsafe_judgment -> constr
 
-(* If [j] is the judgement $c:t:s$, then [typed_type_of_judgment env j]
-   constructs the typed type $t:s$, while [assumption_of_judgement env j]
-   cosntructs the type type $c:t$, checking that $t$ is a sort. *)
+(* If [j] is the judgement $c:t$, then [assumption_of_judgement env j]
+   returns the type $c$, checking that $t$ is a sort. *)
 
-val typed_type_of_judgment : 
-  env -> 'a evar_map -> unsafe_judgment -> typed_type
 val assumption_of_judgment : 
-  env -> 'a evar_map -> unsafe_judgment -> typed_type
-val assumption_of_type_judgment : unsafe_type_judgment -> typed_type
+  env -> 'a evar_map -> unsafe_judgment -> types
+
 val type_judgment : 
   env -> 'a evar_map -> unsafe_judgment -> unsafe_type_judgment
 
 val relative : env -> 'a evar_map -> int -> unsafe_judgment
 
-val type_of_constant : env -> 'a evar_map -> constant -> typed_type
+val type_of_constant : env -> 'a evar_map -> constant -> types
 
-val type_of_inductive : env -> 'a evar_map -> inductive -> typed_type
+val type_of_inductive : env -> 'a evar_map -> inductive -> types
 
-val type_of_constructor : env -> 'a evar_map -> constructor -> typed_type
+val type_of_constructor : env -> 'a evar_map -> constructor -> types
 
 val type_of_existential : env -> 'a evar_map -> constr -> constr
 
@@ -51,22 +48,22 @@ val judge_of_prop_contents : contents -> unsafe_judgment
 
 val judge_of_type : universe -> unsafe_judgment * constraints
 
-val generalize_without_universes : named_declaration -> typed_type -> typed_type
-
+(*s Type of an abstraction. *)
 val abs_rel : 
-  env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
+  env -> 'a evar_map -> name -> types -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
+(*s Type of a product. *)
 val gen_rel :
   env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val sort_of_product : sorts -> sorts -> universes -> sorts * constraints
-val sort_of_product_without_univ : sorts -> sorts -> sorts
 
-val cast_rel : 
-  env -> 'a evar_map -> unsafe_judgment -> unsafe_judgment 
-    -> unsafe_judgment
+(*s Type of a cast. *)
+val cast_rel :
+  env -> 'a evar_map -> unsafe_judgment -> types
+    -> unsafe_judgment * constraints
 
 val apply_rel_list : 
   env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
@@ -76,7 +73,7 @@ val check_fix : env -> 'a evar_map -> fixpoint -> unit
 val check_cofix : env -> 'a evar_map -> cofixpoint -> unit
 val control_only_guard : env -> 'a evar_map -> constr -> unit
 
-val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array 
+val type_fixpoint : env -> 'a evar_map -> name list -> types array 
     -> unsafe_judgment array -> constraints
 
 open Inductive