From 44817bf722eacb0379bebc7e435bfafa503d574f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Oct 2015 14:21:45 +0200
Subject:  Fix #4346 2/2: VM casts were not inferring universe constraints.

---
 pretyping/pretyping.ml | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e1e8982e1e..f6c1867285 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -929,14 +929,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
 	      if not (occur_existential cty || occur_existential tval) then
-		begin 
-		  try
-		    let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in 
-		    ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
-		  with Reduction.NotConvertible -> 
-		    error_actual_type_loc loc env !evdref cj tval 
+		let (evd,b) = Vnorm.vm_infer_conv env !evdref cty tval in
+		if b then (evdref := evd; cj)
+		else
+		  error_actual_type_loc loc env !evdref cj tval 
                       (ConversionFailed (env,cty,tval))
-		end
 	      else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
-- 
cgit v1.2.3