diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-01 22:22:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-01 22:22:24 +0000 |
| commit | 50d21e5c4f9613a2080d71925dd3a747aed70f5d (patch) | |
| tree | e808f620f7bf702860a28807f2ecf841dc67e843 /interp | |
| parent | 17c18b808adde5d8c1b9c11f3b1956b47ded282f (diff) | |
Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_loc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4756 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -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 cd0ac0aa1..a79d98495 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 711e81cc2..483c0b792 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 *) |