From 57c726d52bd47874ec22c9b816aae11f8be366d8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 9 Aug 2014 22:22:05 +0200
Subject: Small optimization in Cooking: do not construct identity
 substitutions.

---
 kernel/cooking.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 589a26134..3dd782342 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -176,7 +176,7 @@ let cook_constr { Opaqueproof.modlist ; abstract } c =
   abstract_constant_body (expmod c) hyps
 
 let lift_univs cb subst =
-  if cb.const_polymorphic then
+  if cb.const_polymorphic && not (Univ.LMap.is_empty subst) then
     let inst = Univ.UContext.instance cb.const_universes in
     let cstrs = Univ.UContext.constraints cb.const_universes in
     let len = Univ.LMap.cardinal subst in
-- 
cgit v1.2.3