diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-14 11:01:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-01-14 11:01:04 +0000 |
| commit | 7aea5b4a925f752c8e056d2ca1e9bfe48a066372 (patch) | |
| tree | 211f73dff64f911a632c951d29ff3c79dd6822d3 /parsing/pcoq.ml4 | |
| 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 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ed4f41c4e..d81727487 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -496,9 +496,6 @@ module Vernac_ = struct let gec_vernac s = Gram.Entry.create ("vernac:" ^ s) - let locality = gec_vernac "locality" - let non_locality = gec_vernac "non_locality" - (* The different kinds of vernacular commands *) let gallina = gec_vernac "gallina" let gallina_ext = gec_vernac "gallina_ext" |