diff options
| author | sacerdot | 2004-09-10 14:09:09 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-10 14:09:09 +0000 |
| commit | 004776ff085651b83a9b102f64f8939ce4a2773d (patch) | |
| tree | 834ed33489a1036bed4b932f26ead38539afc982 /proofs | |
| parent | a4a147005e014bfe2b5d549a0662a88f551bce78 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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) |