aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-09 22:22:05 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-13 12:31:14 +0200
commit57c726d52bd47874ec22c9b816aae11f8be366d8 (patch)
treec1e6bf4580cbf6948e2b0e9c78952693aa714bd4 /kernel
parentbcb425ead1d12d6e800f9f13f28b34da529c463e (diff)
Small optimization in Cooking: do not construct identity substitutions.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml2
1 files changed, 1 insertions, 1 deletions
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