From 004776ff085651b83a9b102f64f8939ce4a2773d Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 10 Sep 2004 14:09:09 +0000
Subject: When refining a given term, the primitive refiner used to accepts
 some casts, but to ignore others. This commit ensures that casts are always
 dealt properly.

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 82994669b9..e7af07dfe7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -353,6 +353,10 @@ and mk_hdgoals sigma goal goalacc trm =
 	check_typability env sigma ty;
 	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
 
+    | Cast (t,ty) ->
+	check_typability env sigma ty;
+	mk_refgoals sigma goal goalacc ty t
+
     | App (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
-- 
cgit v1.2.3