From e506e9fb9164ffaeace23f6280953dd55762e75f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 21 Jul 2010 15:26:48 +0000
Subject: Applied Pierre Letouzey's patch restoring Convert_concl VM casts in
 new proof engine.

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

diff --git a/proofs/logic.ml b/proofs/logic.ml
index db60c6afc0..eddb2fdac9 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -614,10 +614,11 @@ let prim_refiner r sigma goal =
 	  (sgl, sigma)
 
     (* Conversion rules *)
-    | Convert_concl (cl',_) ->
+    | Convert_concl (cl',k) ->
 	check_typability env sigma cl';
 	if (not !check) || is_conv_leq env sigma cl' cl then
           let (sg,ev,sigma) = mk_goal sign cl' in
+	  let ev = if k=VMcast then mkCast(ev,k,cl) else ev in
 	  let sigma = Goal.V82.partial_solution sigma goal ev in
           ([sg], sigma)
 	else
-- 
cgit v1.2.3