Fixed a notation bug when extending binder_constr with empty levels

(see Notations.v).
Improved the "already occurs in a different scope" test and message.



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

4 files changed, 24 insertions, 5 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index aa836ea11e..8b60cff50d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -171,15 +171,26 @@ let contract_pat_notation ntn (l,ll) =
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
-let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
+let make_current_scope = function
+  | (Some tmp_scope,(sc::_ as scopes)) when sc = tmp_scope -> scopes
+  | (Some tmp_scope,scopes) -> tmp_scope::scopes
+  | None,scopes -> scopes
 
 let set_var_scope loc id (_,_,scopt,scopes) varscopes =
   let idscopes = List.assoc id varscopes in
   if !idscopes <> None &
     make_current_scope (Option.get !idscopes)
     <> make_current_scope (scopt,scopes) then
+      let pr_scope_stack = function
+	| [] -> str "the empty scope stack"
+	| [a] -> str "scope " ++ str a
+	| l -> str "scope stack " ++
+	    str "[" ++ prlist_with_sep pr_coma str l ++ str "]" in
       user_err_loc (loc,"set_var_scope",
-      pr_id id ++ str " already occurs in a different scope.")
+      pr_id id ++ str " is used both in " ++ 
+	pr_scope_stack (make_current_scope (Option.get !idscopes)) ++
+	strbrk " and in " ++
+	pr_scope_stack (make_current_scope (scopt,scopes)))
   else
     idscopes := Some (scopt,scopes)
 
diff --git a/interp/notation.mli b/interp/notation.mli
index f3036f226f..3dc3c95c20 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -164,7 +164,7 @@ type symbol =
 val make_notation_key : symbol list -> notation
 val decompose_notation_key : notation -> symbol list
 
-(* Prints scopes (expect a pure aconstr printer *)
+(* Prints scopes (expects a pure aconstr printer) *)
 val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
 val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
 val locate_notation : (rawconstr -> std_ppcmds) -> notation ->
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 8d90499dc2..927ac74e0c 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -116,7 +116,10 @@ let make_constr_prod_item univ assoc from forpat = function
       let eobj = symbol_of_constr_prod_entry_key assoc from forpat nt in
       (eobj, Option.map (fun x -> (x,nt)) ovar)
 
-let prepare_empty_levels entry (pos,p4assoc,name,reinit) =
+let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
+  let entry = 
+    if forpat then weaken_entry Constr.pattern
+    else weaken_entry Constr.operconstr in
   grammar_extend entry pos reinit [(name, p4assoc, [])]
 
 let pure_sublevels level symbs =
@@ -133,7 +136,7 @@ let extend_constr (entry,level) (n,assoc) mkact forpat pt =
   let pure_sublevels = pure_sublevels level symbs in
   let needed_levels = register_empty_levels forpat pure_sublevels in
   let pos,p4assoc,name,reinit = find_position forpat assoc level in
-  List.iter (prepare_empty_levels entry) needed_levels;
+  List.iter (prepare_empty_levels forpat) needed_levels;
   grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])]
 
 let extend_constr_notation (n,assoc,ntn,rule) =
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 1bff749335..b09c6c9a74 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -43,3 +43,8 @@ Notation "'exists' x , P" := (x, P)
    (at level 200, x ident, right associativity,	only parsing).
 
 Definition foo P := let '(exists x, Q) := P in x = Q :> nat.
+
+(* Check empty levels when extending binder_constr *)
+
+Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat
+   (at level 200, x ident, right associativity, y at level 69).