diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 27 |
1 files changed, 14 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 |