Merge PR #1109: Handle some misc todos

3 files changed, 15 insertions, 17 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index d2b41aae9..8568bf14b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -166,16 +166,10 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
       let mb_mp1 = lookup_module mp1 env in
       let mtb_mp1 = module_type_of_module mb_mp1 in
       let cst = match old.mod_expr with
-	| Abstract ->
-	  begin
-            try
-              let mtb_old = module_type_of_module old in
-              let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
-              Univ.ContextSet.add_constraints chk_cst old.mod_constraints
-	    with Failure _ ->
-              (* TODO: where can a Failure come from ??? *)
-              error_incorrect_with_constraint lab
-	  end
+        | Abstract ->
+          let mtb_old = module_type_of_module old in
+          let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
+          Univ.ContextSet.add_constraints chk_cst old.mod_constraints
 	| Algebraic (NoFunctor (MEident(mp'))) ->
 	  check_modpath_equiv env' mp1 mp';
 	  old.mod_constraints
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 044877e82..b40badd7c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -65,6 +65,10 @@ let type_of_type u =
   let uu = Universe.super u in
     mkType uu
 
+let type_of_sort = function
+  | Prop c -> type1
+  | Type u -> type_of_type u
+
 (*s Type of a de Bruijn index. *)
 
 let type_of_relative env n =
@@ -323,11 +327,7 @@ let rec execute env cstr =
   let open Context.Rel.Declaration in
   match kind_of_term cstr with
     (* Atomic terms *)
-    | Sort (Prop c) ->
-      type1
-	
-    | Sort (Type u) ->
-      type_of_type u
+    | Sort s -> type_of_sort s
 
     | Rel n ->
       type_of_relative env n
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a8f7fba9a..96be6c14a 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -37,15 +37,19 @@ val assumption_of_judgment :  env -> unsafe_judgment -> types
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
 
 (** {6 Type of sorts. } *)
+val type1 : types
+val type_of_sort : Sorts.t -> types
 val judge_of_prop : unsafe_judgment
 val judge_of_set  : unsafe_judgment
 val judge_of_prop_contents  : contents -> unsafe_judgment
 val judge_of_type           : universe -> unsafe_judgment
 
 (** {6 Type of a bound variable. } *)
+val type_of_relative : env -> int -> types
 val judge_of_relative : env -> int -> unsafe_judgment
 
 (** {6 Type of variables } *)
+val type_of_variable : env -> variable -> types
 val judge_of_variable : env -> variable -> unsafe_judgment
 
 (** {6 type of a constant } *)
@@ -66,9 +70,9 @@ val judge_of_abstraction :
   env -> Name.t -> unsafe_type_judgment -> unsafe_judgment
     -> unsafe_judgment
 
-val sort_of_product : env -> sorts -> sorts -> sorts
-
 (** {6 Type of a product. } *)
+val sort_of_product : env -> sorts -> sorts -> sorts
+val type_of_product : env -> Name.t -> sorts -> sorts -> types
 val judge_of_product :
   env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment
     -> unsafe_judgment