From b824d8ad00001f6c41d0fc8bbf528dccb937c887 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 20:25:05 +0200
Subject: Restore a fast path in EConstr instance normalization.

---
 engine/eConstr.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 28e9ffdb27..bb9075e74a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -63,7 +63,9 @@ module EInstance =
 struct
   type t = Univ.Instance.t
   let make i = i
-  let kind sigma i = Evd.normalize_universe_instance sigma i
+  let kind sigma i =
+    if Univ.Instance.is_empty i then i
+    else Evd.normalize_universe_instance sigma i
   let empty = Univ.Instance.empty
   let is_empty = Univ.Instance.is_empty
   let unsafe_to_instance t = t
-- 
cgit v1.2.3