From e781fdf9a135526e67ebb014412c663d54ef9e28 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 10 Jun 2014 19:27:58 +0200
Subject: In generalized rewrite, avoid retyping completely and constantly the
 conclusion, and results of unifying the lemma with subterms. Using
 Retyping.get_type_of instead results in 3x speedup in Ncring_polynom.

---
 kernel/univ.ml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index cc1b083d87..3a8724dd5c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -536,6 +536,10 @@ struct
     let is_prop = function
       | (l,0) -> Level.is_prop l
       | _ -> false
+	
+    let is_small = function
+      | (l,0) -> Level.is_small l
+      | _ -> false
 
     let equal x y = x == y ||
       (let (u,n) = x and (v,n') = y in
@@ -642,8 +646,8 @@ struct
     fold (fun x acc -> LSet.add (Expr.get_level x) acc) l LSet.empty
 
   let is_small u = 
-    match level u with
-    | Some l -> Level.is_small l
+    match node u with
+    | Cons (l, n) when is_nil n -> Expr.is_small l
     | _ -> false
 
   (* The lower predicative level of the hierarchy that contains (impredicative)
@@ -663,7 +667,9 @@ struct
   (* Returns the formal universe that lies juste above the universe variable u.
      Used to type the sort u. *)
   let super l = 
-    Huniv.map (fun x -> Expr.successor x) l
+    if is_small l then type1
+    else
+      Huniv.map (fun x -> Expr.successor x) l
 
   let addn n l =
     Huniv.map (fun x -> Expr.addn n x) l
-- 
cgit v1.2.3