From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 tactics/btermdn.ml | 62 +++++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 50 insertions(+), 12 deletions(-)

(limited to 'tactics/btermdn.ml')

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index f0b23b8d..a0aecbbc 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -6,9 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: btermdn.ml 6427 2004-12-07 17:41:10Z sacerdot $ *)
+(* $Id: btermdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Term
+open Names
 open Termdn
 open Pattern
 open Libnames
@@ -19,6 +20,23 @@ open Libnames
 
 let dnet_depth = ref 8
 		   
+let bounded_constr_pat_discr_st st (t,depth) =
+  if depth = 0 then 
+    None 
+  else
+    match constr_pat_discr_st st t with
+      | None -> None
+      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+	    
+let bounded_constr_val_discr_st st (t,depth) =
+  if depth = 0 then 
+    Dn.Nothing 
+  else
+    match constr_val_discr_st st t with
+      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+      | Dn.Nothing -> Dn.Nothing
+      | Dn.Everything -> Dn.Everything
+
 let bounded_constr_pat_discr (t,depth) =
   if depth = 0 then 
     None 
@@ -29,24 +47,44 @@ let bounded_constr_pat_discr (t,depth) =
 	    
 let bounded_constr_val_discr (t,depth) =
   if depth = 0 then 
-    None 
+    Dn.Nothing 
   else
     match constr_val_discr t with
-      | None -> None
-      | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
+      | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l)
+      | Dn.Nothing -> Dn.Nothing
+      | Dn.Everything -> Dn.Everything
 
 type 'a t = (global_reference,constr_pattern * int,'a) Dn.t
-
+  
 let create = Dn.create
+  
+let add = function
+  | None -> 
+      (fun dn (c,v) -> 
+	Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+  | Some st -> 
+      (fun dn (c,v) -> 
+	Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
 
-let add dn (c,v) = Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)
-
-let rmv dn (c,v) = Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)
+let rmv = function
+  | None -> 
+      (fun dn (c,v) -> 
+	Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
+  | Some st -> 
+      (fun dn (c,v) -> 
+	Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
 
-let lookup dn t =
-  List.map 
-    (fun ((c,_),v) -> (c,v)) 
-    (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))
+let lookup = function
+  | None -> 
+      (fun dn t ->
+	List.map 
+	  (fun ((c,_),v) -> (c,v)) 
+	  (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)))
+  | Some st -> 
+      (fun dn t ->
+	List.map 
+	  (fun ((c,_),v) -> (c,v)) 
+	  (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth)))
 
 let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn
 
-- 
cgit v1.2.3