aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-24 22:28:26 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-24 22:28:26 +0000
commitdac45df4c768349454e5fb950b7a566a600af597 (patch)
tree1c764c45719f24f9082334b9018b34d47368d311 /INSTALL
parent8a5f877b257133d12045e11ada64674e5a481ae6 (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 'INSTALL')
0 files changed, 0 insertions, 0 deletions