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 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/typeops.ml')

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
-- 
cgit v1.2.3