From 50d21e5c4f9613a2080d71925dd3a747aed70f5d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Nov 2003 22:22:24 +0000
Subject: 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
---
 interp/symbols.ml  | 9 ++++++++-
 interp/symbols.mli | 2 ++
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'interp')

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 *)
-- 
cgit v1.2.3