Fix a small notation/scope bug:

When defining an inductive type with a reserved notation in a 
particuliar scope, the scope was not opened during the interpretation.



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

3 files changed, 27 insertions, 1 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index bb17eda2c9..e6c627e863 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -92,6 +92,11 @@ let scope_stack = ref []
 
 let current_scopes () = !scope_stack
 
+let scope_is_open_in_scopes sc l = 
+  List.mem (Scope sc) l
+
+let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) 
+
 (* TODO: push nat_scope, z_scope, ... in scopes summary *)
 
 (* Exportation of scopes *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 35d1c0d17b..06349014db 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -39,6 +39,11 @@ val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
 
+(* Check where a scope is opened or not in a scope list, or in
+ * the current opened scopes *)
+val scope_is_open_in_scopes : scope_name -> scopes -> bool
+val scope_is_open : scope_name -> bool
+
 (* Open scope *)
 
 val open_close_scope : 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4fb56dfd66..83a380ed52 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -465,7 +465,15 @@ let compute_interning_datas env ty l nal typl impll =
   (l, list_map3 mk_interning_data nal typl impll)
 
 let declare_interning_data (_,impls) (df,c,scope) =
-  silently (Metasyntax.add_notation_interpretation df impls c) scope
+  silently (fun sc ->
+    Metasyntax.add_notation_interpretation df impls c sc;
+    (* Temporary opening of scopes for interpretation
+     of notations in mutual inductive types *)
+    match sc with 
+     | None -> ()
+     | Some sc -> if not (Notation.scope_is_open sc)
+        then Notation.open_close_scope (false,true,sc)
+     ) scope
 
 let push_named_types env idl tl =
   List.fold_left2 (fun env id t -> Environ.push_named (id,None,t) env)
@@ -654,10 +662,18 @@ let build_mutual l finite =
   let coes = extract_coercions indl in
   let notations,indl = prepare_inductive ntnl indl in
   let mie,impls = interp_mutual paramsl indl notations finite in
+  let cur_scopes = Notation.current_scopes() in 
+  let temp_scopes = List.map (fun (_,_,sc) -> sc) notations in
   (* Declare the mutual inductive block with its eliminations *)
   ignore (declare_mutual_with_eliminations false mie impls);
   (* Declare the possible notations of inductive types *)
   List.iter (declare_interning_data ([],[])) notations;
+  (* Close temporary opened scope for interpretation of mutual ind *)
+  List.iter (function
+    | None -> ()
+    | Some sc ->
+      if not (Notation.scope_is_open_in_scopes sc cur_scopes)
+      then Notation.open_close_scope (false,false,sc) ) temp_scopes; 
   (* Declare the coercions *)
   List.iter (fun qid -> Class.try_add_new_coercion (locate qid) Global) coes