Improving management of notations with binders (see #2708 where a

variable is used both as term and as binder, resulting in
ununderstandable error message about scopes).

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

2 files changed, 19 insertions, 13 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 880afe57d2..d886d8a605 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -280,8 +280,9 @@ let pr_scope_stack = function
 
 let error_inconsistent_scope loc id scopes1 scopes2 =
   user_err_loc (loc,"set_var_scope",
-    pr_id id ++ str " is used both in " ++
-    pr_scope_stack scopes1 ++ strbrk " and in " ++ pr_scope_stack scopes2)
+    pr_id id ++ str " is here used in " ++
+    pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++
+    pr_scope_stack scopes1)
 
 let error_expect_constr_notation_type loc id =
   user_err_loc (loc,"",
@@ -295,17 +296,17 @@ let error_expect_binder_notation_type loc id =
 let set_var_scope loc id istermvar env ntnvars =
   try
     let idscopes,typ = List.assoc id ntnvars in
-    if !idscopes <> None &
-      (* scopes have no effect on the interpretation of identifiers, hence
-         we can tolerate having a variable occurring several times in
-         different scopes: *) typ <> NtnInternTypeIdent &
-      make_current_scope (Option.get !idscopes)
-      <> make_current_scope (env.tmp_scope,env.scopes) then
-	error_inconsistent_scope loc id
-	  (make_current_scope (Option.get !idscopes))
-	  (make_current_scope (env.tmp_scope,env.scopes))
-    else
-      idscopes := Some (env.tmp_scope,env.scopes);
+    if istermvar then
+      (* scopes have no effect on the interpretation of identifiers *)
+      if !idscopes = None then
+        idscopes := Some (env.tmp_scope,env.scopes)
+      else
+        if make_current_scope (Option.get !idscopes)
+          <> make_current_scope (env.tmp_scope,env.scopes)
+        then
+	  error_inconsistent_scope loc id
+	    (make_current_scope (Option.get !idscopes))
+	    (make_current_scope (env.tmp_scope,env.scopes));
     match typ with
     | NtnInternTypeBinder ->
 	if istermvar then error_expect_binder_notation_type loc id
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 89f1105937..2371d32cda 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -96,3 +96,8 @@ Notation "'FORALL'  x .. y , P" := (forall x, .. (forall y, P) ..)
   (at level 200, x binder, y binder, right associativity) : type_scope.
 
 Fail Check fun x => match x with S (FORALL x, _) => 0 end.
+
+(* Bug #2708: don't check for scope of variables used as binder *)
+
+Parameter traverse : (nat -> unit) -> (nat -> unit).
+Notation traverse_var f l := (traverse (fun l => f l) l).