From 98e8b75b640c93abc63140ce1fc3dc445d775066 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Tue, 15 May 2012 11:54:01 +0000
Subject: Notations are back in the "in" clause of pattern matching.

Fixes the test-suite.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 102d42c213..72a7138669 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -387,6 +387,9 @@ let uninterp_notations c =
 let uninterp_cases_pattern_notations c =
   Gmapl.find (cases_pattern_key c) !notations_key_table
 
+let uninterp_ind_pattern_notations ind =
+  Gmapl.find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
+
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
     Gmap.mem ntn (Gmap.find scope !scope_map).notations in
@@ -401,6 +404,20 @@ let uninterp_prim_token c =
       | Some n -> (sc,n)
   with Not_found -> raise No_match
 
+let uninterp_prim_token_ind_pattern ind args =
+  let ref = IndRef ind in
+  try
+    let (sc,numpr,b) = Hashtbl.find prim_token_key_table
+      (RefKey (canonical_gr ref)) in
+    if not b then raise No_match;
+    let args' = List.map
+      (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
+    let ref = GRef (dummy_loc,ref) in
+    match numpr (GApp (dummy_loc,ref,args')) with
+      | None -> raise No_match
+      | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
 let uninterp_prim_token_cases_pattern c =
   try
     let k = cases_pattern_key c in
-- 
cgit v1.2.3