diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-11 19:19:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-11 19:19:04 +0000 |
| commit | bc1ddb1081dd44887cb2f8b33937138cb1e1658c (patch) | |
| tree | 396f99140c055245ae45cda6afd68462634c0191 /plugins/micromega/sos.ml | |
| parent | b0dd26994fcc609668466d969dd88d9a008030e2 (diff) | |
Improving a few error messages in Ltac interpretation
- improving error message when a reference to unfold is not found
- repairing anomaly when an evaluable reference exists at
internalisation-time but not at run time, and similarly for an
arbitrary term (but the latter is new from 8.3 because of the new
use of retyping instead of understand for typing Ltac values)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13408 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/sos.ml')
0 files changed, 0 insertions, 0 deletions