diff options
| author | herbelin | 2009-01-14 11:01:04 +0000 |
|---|---|---|
| committer | herbelin | 2009-01-14 11:01:04 +0000 |
| commit | 7aea5b4a925f752c8e056d2ca1e9bfe48a066372 (patch) | |
| tree | 211f73dff64f911a632c951d29ff3c79dd6822d3 /contrib/xml/xmlcommand.ml | |
| parent | f25c1f790bb41466c12d2eb232fff9b82b3e1f26 (diff) | |
Fixing/improving management of uniform prefix Local and Global
modifiers (added a "Syntax Checking" phase for raising a non
interpretation error just after a dot is parsed -- maybe exaggerated
complication for what we want to do ?).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11783 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions