diff options
| -rw-r--r-- | interp/constrintern.ml | 27 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 5 |
2 files changed, 19 insertions, 13 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 880afe57d..d886d8a60 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 89f110593..2371d32cd 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). |