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.

---
 pretyping/pretyping.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dff1b9772f..cb6deb41cb 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -318,11 +318,12 @@ let pretype_ref loc evdref env ref us =
       make_judge c ty
 
 let judge_of_Type evd s =
-  let judge s = 
+  let evd, l = interp_universe_name evd s in
+  let s = Univ.Universe.make l in
+  let judge = 
     { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
   in
-  let evd, l = interp_universe_name evd s in
-    evd, judge (Univ.Universe.make l)
+    evd, judge
 
 let pretype_sort evdref = function
   | GProp -> judge_of_prop
-- 
cgit v1.2.3