diff options
| author | herbelin | 2012-07-21 21:12:00 +0000 |
|---|---|---|
| committer | herbelin | 2012-07-21 21:12:00 +0000 |
| commit | 35087ab8adb906c37f185e14b183a93b2f6b22aa (patch) | |
| tree | 9bd3b156c36d19b1b799c82da82beb92c87fa4b7 /interp | |
| parent | ff9f3714fcbaef1b2ddea3ba3ddde42c5d38014c (diff) | |
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
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 |