From 266aea59645ede8fc12ff60ce077504e1f29624c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 9 Apr 2014 14:02:15 +0200
Subject: Keep track of universes on coercion applications even if they're not
 polymorphic (fixes bug #3043).

---
 pretyping/coercion.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/coercion.ml')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ab3a3fa100..baa9086166 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -335,7 +335,7 @@ let apply_coercion env sigma p hj typ_cl =
 	  let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
 	  let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 	  let sigma, jres = 
-	    apply_coercion_args env sigma (not (Univ.ContextSet.is_empty ctx)) argl fv 
+	    apply_coercion_args env sigma true argl fv 
 	  in
 	    (if isid then
 	      { uj_val = ja.uj_val; uj_type = jres.uj_type }
-- 
cgit v1.2.3