diff options
| -rw-r--r-- | interp/notation.ml | 26 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 11 |
2 files changed, 25 insertions, 12 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 9967a8e5e..8f19ab851 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -322,17 +322,18 @@ let declare_uninterpretation rule (metas,c as pat) = let (key,n) = aconstr_key c in notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table -let rec find_interpretation find = function +let rec find_interpretation ntn find = function | [] -> raise Not_found - | sce :: scopes -> - let sc,sco = match sce with - | Scope sc -> sc, Some sc - | SingleNotation _ -> default_scope, None in - try - let (pat,df) = find sc in - pat,(df,sco) - with Not_found -> - find_interpretation find scopes + | Scope scope :: scopes -> + (try let (pat,df) = find scope in pat,(df,Some scope) + with Not_found -> find_interpretation ntn find scopes) + | SingleNotation ntn'::scopes when ntn' = ntn -> + (try let (pat,df) = find default_scope in pat,(df,None) + with Not_found -> + (* e.g. because single notation only for constr, not cases_pattern *) + find_interpretation ntn find scopes) + | SingleNotation _::scopes -> + find_interpretation ntn find scopes let find_notation ntn sc = Gmap.find ntn (find_scope sc).notations @@ -355,7 +356,8 @@ let find_prim_token g loc p sc = let interp_prim_token_gen g loc p local_scopes = let scopes = make_current_scopes local_scopes in - try find_interpretation (find_prim_token g loc p) scopes + let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in + try find_interpretation p_as_ntn (find_prim_token g loc p) scopes with Not_found -> user_err_loc (loc,"interp_prim_token", (match p with @@ -370,7 +372,7 @@ let interp_prim_token_cases_pattern loc p name = let rec interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in - try find_interpretation (find_notation ntn) scopes + try find_interpretation ntn (find_notation ntn) scopes with Not_found -> user_err_loc (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index ddad217b3..f5f5a9d14 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -75,3 +75,14 @@ End B. (* Should succeed *) Definition n := 5 * 5. + +(* Check that lonely notations (here FOO) do not modify the visibility + of scoped interpretations (bug #2634 fixed in r14819) *) + +Notation "x ++++ y" := (mult x y) (at level 40). +Notation "x ++++ y" := (plus x y) : A_scope. +Open Scope A_scope. +Notation "'FOO' x" := (S x) (at level 40). +Goal (2 ++++ 3) = 5. +reflexivity. +Abort. |