diff options
| -rw-r--r-- | proofs/logic.ml | 12 |
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) = |