diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-24 22:28:26 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-24 22:28:26 +0000 |
| commit | dac45df4c768349454e5fb950b7a566a600af597 (patch) | |
| tree | 1c764c45719f24f9082334b9018b34d47368d311 /proofs/clenvtac.ml | |
| parent | 8a5f877b257133d12045e11ada64674e5a481ae6 (diff) | |
Raise informative errors instead of Failures or anomalies in case a meta
type contains a meta as this is currently unsupported in the
refiner. Fixes bugs #1980 and #1981.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11501 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 5c204c8bb..f368ed379 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -54,7 +54,8 @@ let clenv_cast_meta clenv = (match Evd.find_meta clenv.evd mv with | Clval (_,(body,_),_) -> body.rebus | Cltyp (_,typ) -> - assert (not (occur_meta typ.rebus)); + if occur_meta typ.rebus then + raise (RefinerError (MetaInType typ.rebus)); mkCast (mkMeta mv, DEFAULTcast, typ.rebus)) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) | Case(ci,p,c,br) -> mkCase (ci, crec p, crec_hd c, Array.map crec br) |