From ce5c8001eefebd4d7951a88f6171f92c924e8b0c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 29 Sep 2017 14:37:09 +0200
Subject: Remove some duplication between Typeops and Nativenorm.

---
 kernel/typeops.ml  | 10 +++++-----
 kernel/typeops.mli |  8 ++++++--
 2 files changed, 11 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 044877e82a..b40badd7c8 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 a8f7fba9a0..96be6c14a4 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
-- 
cgit v1.2.3


From 0932339dbf44e4ef2b04426f7b4ac6d74b2f4f1f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 29 Sep 2017 16:20:11 +0200
Subject: Remove unused Failure catch

Unused since dc57718e98289b5d71a0a942d6a063d441dc6a54 as far as I can
tell.
---
 kernel/mod_typing.ml | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

(limited to 'kernel')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index d2b41aae98..8568bf14b8 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
-- 
cgit v1.2.3