Ajout option "Local" à "Open Scope"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3867 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 10 insertions, 7 deletions

diff --git a/interp/symbols.ml b/interp/symbols.ml
index 6a02f284b1..662153f782 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -293,7 +293,7 @@ let exists_notation prec nt =
     !scope_map false 
 
 (* Exportation of scopes *)
-let cache_scope (_,sc) =
+let cache_scope (_,(exp,sc)) =
   check_scope sc;
   scope_stack := sc :: !scope_stack
 
@@ -307,7 +307,7 @@ let (inScope,outScope) =
       open_function = (fun i o -> if i=1 then cache_scope o);
       subst_function = subst_scope;
       classify_function = (fun (_,o) -> Substitute o);
-      export_function = (fun x -> Some x) }
+      export_function = (fun (exp,_ as x) -> if exp then Some x else None) }
 
 let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
 
diff --git a/interp/symbols.mli b/interp/symbols.mli
index c8c844312d..42eedaf81c 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -39,7 +39,7 @@ val declare_scope : scope_name -> unit
 (* Open scope *)
 
 val current_scopes : unit -> scopes
-val open_scope : scope_name -> unit
+val open_scope : bool * scope_name -> unit
 
 (* Declare delimiters for printing *)
 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index f1b8b55750..3d97537832 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -245,7 +245,8 @@ GEXTEND Gram
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
 	 -> VernacSyntaxExtension (s,l)
 
-     | IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc
+     | IDENT "Open"; exp = [IDENT "Local" -> false | -> true]; IDENT "Scope"; 
+	 sc = IDENT -> VernacOpenScope (exp,sc)
 
      | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 12e95d235a..0ad8caaaa0 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -648,7 +648,8 @@ GEXTEND Gram
   GLOBAL: syntax;
 
   syntax:
-   [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc
+   [ [ IDENT "Open"; exp = [IDENT "Local" -> false | -> true]; IDENT "Scope"; 
+       sc = IDENT -> VernacOpenScope (exp,sc)
 
      | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c332e894ad..171238eb87 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -154,7 +154,7 @@ type vernac_expr =
   | VernacDistfix of
       grammar_associativity * precedence * string * reference *
       scope_name option
-  | VernacOpenScope of scope_name
+  | VernacOpenScope of (export_flag * scope_name)
   | VernacDelimiters of scope_name * string
   | VernacArgumentsScope of reference * scope_name option list
   | VernacInfix of
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 8e7aa2fc1c..76771ece7c 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -415,7 +415,8 @@ let rec pr_vernac = function
   | VernacTacticGrammar l -> hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***)
   | VernacSyntax (u,el) -> hov 1 (str"Syntax " ++ str u ++ spc() ++
     prlist_with_sep sep_v2 pr_syntax_entry el) (***)
-  | VernacOpenScope sc -> str"Open Scope" ++ spc() ++ str sc
+  | VernacOpenScope (exp,sc) ->
+      str ("Open "^(if exp then "" else "Local ")^"Scope") ++ spc() ++ str sc
   | VernacDelimiters (sc,key) ->
       str"Delimits Scope" ++ spc () ++ str sc ++
       spc() ++ str "with " ++ str key