diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-06 13:33:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-06 13:33:07 +0000 |
| commit | 098d38249daae1ead55ccc1bf04faabcaa47d464 (patch) | |
| tree | 36037718c70922e5af81ac42a844c418eef98f4a /parsing/g_vernac.ml4 | |
| parent | 3e7c148472265c6066633bf39a63bfe387ba9351 (diff) | |
Practical fix for bug #1206 (anomaly raised in pretyping instead of
error when called on ill-typed term, because pretyping called retyping
which in turn is expected to be called only with typable arguments).
Incidentally, #1206 shows once more time the problem of confusion
between section variables (which morally don't have to be cleared) and
their copy in goal (which can be cleared).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15533 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
0 files changed, 0 insertions, 0 deletions