diff options
| -rw-r--r-- | interp/symbols.ml | 9 | ||||
| -rw-r--r-- | interp/symbols.mli | 2 |
2 files changed, 10 insertions, 1 deletions
diff --git a/interp/symbols.ml b/interp/symbols.ml index cd0ac0aa13..a79d98495b 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -169,6 +169,10 @@ let rawconstr_key = function | RRef (_,ref) -> RefKey ref | _ -> Oth +let cases_pattern_key = function + | PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref) + | _ -> Oth + let aconstr_key = function | AApp (ARef ref,args) -> RefKey ref, Some (List.length args) | ARef ref -> RefKey ref, Some 0 @@ -294,6 +298,9 @@ let rec interp_notation ntn scopes = let uninterp_notations c = Gmapl.find (rawconstr_key c) !notations_key_table +let uninterp_cases_pattern_notations c = + Gmapl.find (cases_pattern_key c) !notations_key_table + let availability_of_notation (ntn_scope,ntn) scopes = let f scope = Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in @@ -461,7 +468,7 @@ let pr_scope_classes sc = spc() ++ prlist_with_sep spc pr_class l) ++ fnl() let rec rawconstr_of_aconstr () x = - map_aconstr_with_binders_loc dummy_loc (fun id () -> (id,())) + rawconstr_of_aconstr_with_binders dummy_loc (fun id () -> (id,())) rawconstr_of_aconstr () x let pr_notation_info prraw ntn c = diff --git a/interp/symbols.mli b/interp/symbols.mli index 711e81cc27..483c0b792d 100644 --- a/interp/symbols.mli +++ b/interp/symbols.mli @@ -98,6 +98,8 @@ val interp_notation : notation -> scope_name list -> interpretation (* Returns the possible notations for a given term *) val uninterp_notations : rawconstr -> (interp_rule * interpretation * int option) list +val uninterp_cases_pattern_notations : cases_pattern -> + (interp_rule * interpretation * int option) list (* Test if a notation is available in the scopes *) (* context [scopes] if available, the result is not None; the first *) |