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

1 files changed, 17 insertions, 1 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4fb56dfd6..83a380ed5 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