diff options
| author | herbelin | 2009-10-17 20:28:23 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-17 20:28:23 +0000 |
| commit | 6b391cc61a35d1ef42f88d18f9c428c369180493 (patch) | |
| tree | c402fcb05a8dd450dca2191607c11351633cfac0 /interp | |
| parent | 9d7a9ab7c8182dff99d5afd078747f5d6b1247f0 (diff) | |
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
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 15 | ||||
| -rw-r--r-- | interp/notation.mli | 2 |
2 files changed, 14 insertions, 3 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 -> |