From 1a57766209ad896552be615bd5d839a3b292d041 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Jan 2011 16:38:04 +0000
Subject: Fixing an uncaught exception bug with use of vmcast (backport from
 8.3)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13781 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml        | 5 ++++-
 test-suite/success/conv_pbs.v | 5 +++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a2fb8ea12d..1a5de0c50f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -636,7 +636,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		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) ->
-		      ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
+		     (try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
+                      with Reduction.NotConvertible ->
+                        error_actual_type_loc loc env !evdref cj tval)
+
 		  | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
 		in
 		let v = mkCast (cj.uj_val, k, tval) in
diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v
index f6ebacaea5..05d2c98fa9 100644
--- a/test-suite/success/conv_pbs.v
+++ b/test-suite/success/conv_pbs.v
@@ -221,3 +221,8 @@ with universal_completeness_stoup (Gamma:context)(A:formula){struct A}
           (ProofForallL x t (subst_formula (remove_assoc _ x rho) A)
           (eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _)))))
   end.
+
+
+(* A simple example that raised an uncaught exception at some point *)
+
+Fail Check fun x => @eq_refl x <: true = true.
-- 
cgit v1.2.3