diff options
| author | ppedrot | 2012-01-20 20:13:51 +0000 |
|---|---|---|
| committer | ppedrot | 2012-01-20 20:13:51 +0000 |
| commit | 033d8f9628c54218378ee539648b6df6bfcbdb1e (patch) | |
| tree | 83d2d5236a88be2dff6e6c22c57a432444ca1f79 | |
| 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
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 4 |
4 files changed, 3 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 10bf3f35a2..814ff9a397 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 6340e767f4..075440f1c6 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 6610779254..bba0e56022 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 *) diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index de994d915b..89fbd6ffa4 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -52,8 +52,8 @@ GEXTEND Gram GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac; subtac_gallina_loc: - [ [ Vernac.locality; g = Vernac.gallina -> loc, g - | Vernac.locality; g = Vernac.gallina_ext -> loc, g ] ] + [ [ g = Vernac.gallina -> loc, g + | g = Vernac.gallina_ext -> loc, g ] ] ; subtac_withtac: |