From 61a79f62fa860da63e968b04da9935597312c07e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 8 Apr 2014 16:07:50 +0200
Subject: Correct universe handling in program coercions (bug #2378).

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

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 4254c8188b..ab3a3fa100 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -165,7 +165,9 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		in
 		  aux (hdy :: tele) (subst1 hdx restT) 
 		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
-	else Some co
+	else Some (fun x -> 
+	  let term = co x in
+	    Typing.solve_evars env evdref term)
       in
 	if isEvar c || isEvar c' then
 	  (* Second-order unification needed. *)
-- 
cgit v1.2.3