From 033d8f9628c54218378ee539648b6df6bfcbdb1e Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 20 Jan 2012 20:13:51 +0000 Subject: 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 --- parsing/g_vernac.ml4 | 2 +- parsing/pcoq.ml4 | 1 - parsing/pcoq.mli | 2 -- 3 files changed, 1 insertion(+), 4 deletions(-) (limited to 'parsing') 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 *) -- cgit v1.2.3