From 6668aecbd325d77e6d04e09931eefcabbe8342bf Mon Sep 17 00:00:00 2001
From: bgregoir
Date: Tue, 11 Jan 2011 14:19:05 +0000
Subject: ratrapage exception, deja fait ...

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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1a5de0c50f..1ea2dbd002 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -636,10 +636,12 @@ 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) ->
-		     (try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
-                      with Reduction.NotConvertible ->
-                        error_actual_type_loc loc env !evdref cj tval)
-
+		      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
 		  | _ -> 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