From a430afe4bdc1161a952e02b41acf5efd94609c26 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 May 2011 11:40:04 +0000
Subject: Failing instead of switching to the coercion mechanism when VMcast
 involves evars (seem cleaner) at type-inference time.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14123 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4a0fe9cd24..afbfae3bab 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -629,13 +629,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
  		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
 		let cj = match k with
-		  | VMcast when not (occur_existential cty || occur_existential tval) ->
+		  | VMcast ->
+                      if not (occur_existential cty || occur_existential tval) then
 		      begin 
 			try 
 			  ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
 			with Reduction.NotConvertible -> 
 			  error_actual_type_loc loc env !evdref cj tval 
 		      end
+                      else user_err_loc (loc,"",str "Cannot check cast with vm: unresolved arguments remain.")
 		  | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
 		in
 		let v = mkCast (cj.uj_val, k, tval) in
-- 
cgit v1.2.3