diff options
| author | herbelin | 2010-12-02 17:43:56 +0000 |
|---|---|---|
| committer | herbelin | 2010-12-02 17:43:56 +0000 |
| commit | e895f9ca19247f4fe58833f91e948e200bc9a6e5 (patch) | |
| tree | b6be61c1a3c94e8db8ed2f293ce8ad6b56fbcb6b /lib | |
| parent | 6342bc95a166d224ea64f1e3b8977e4f3560b485 (diff) | |
Fixing a bug introduced in r12304 (move of interpretation of
Local/Global modifiers in interpretation loop so as to support
Local/Global for grammar extension) that made use of
DuringSyntaxChecking error wrapper inappropriately nested with the
DuringCommandInterp error wrapper, what disturbed the error
processors. Good thing, we can now simplify things and completely
remove the DuringSyntaxChecking wrapper.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13667 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions