diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-20 20:13:51 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-01-20 20:13:51 +0000 |
| commit | 033d8f9628c54218378ee539648b6df6bfcbdb1e (patch) | |
| tree | 83d2d5236a88be2dff6e6c22c57a432444ca1f79 /parsing | |
| parent | 15f7e93adeb4342f6c255bdb2cf624a98b28034a (diff) | |
Reverted previous commit, which broke library compilation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14925 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
3 files changed, 1 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 10bf3f35a..814ff9a39 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -69,7 +69,7 @@ let default_command_entry = let no_hook _ _ = () GEXTEND Gram - GLOBAL: vernac gallina_ext locality tactic_mode noedit_mode subprf subgoal_command; + GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6340e767f..075440f1c 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -419,7 +419,6 @@ module Vernac_ = let vernac = gec_vernac "Vernac.vernac" let vernac_eoi = eoi_entry vernac let rec_definition = gec_vernac "Vernac.rec_definition" - let locality = gec_vernac "locality" (* Main vernac entry *) let main_entry = Gram.entry_create "vernac" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 661077925..bba0e5602 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -237,8 +237,6 @@ module Vernac_ : val vernac : vernac_expr Gram.entry val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry val vernac_eoi : vernac_expr Gram.entry - (* FIXME: hack to handle locality in Program *) - val locality : unit Gram.entry end (** The main entry: reads an optional vernac command *) |