Attempt to preserve casts during a refine, especially VMcast

placed by vm_cast_no_check

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13703 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 2 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5b55e1c02..2835eb542 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -337,10 +337,18 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	  let (gl,ev,sigma) = mk_goal hyps conclty in
 	  gl::goalacc, conclty, sigma, ev
 
-    | Cast (t,_, ty) ->
+    | Cast (t,k, ty) ->
 	check_typability env sigma ty;
 	check_conv_leq_goal env sigma trm ty conclty;
-	mk_refgoals sigma goal goalacc ty t
+	let res = mk_refgoals sigma goal goalacc ty t in
+	(** we keep the casts (in particular VMcast) except
+	    when they are annotating metas *)
+	if isMeta t then begin
+	  assert (k <> VMcast);
+	  res
+	end else
+	  let (gls,cty,sigma,trm) = res in
+	  (gls,cty,sigma,mkCast(trm,k,ty))
 
     | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =