Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

1 files changed, 9 insertions, 5 deletions

diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index d9d0a799..b94ae2dd 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nbtermdn.ml 10346 2007-12-05 21:11:19Z aspiwack $ *)
+(* $Id: nbtermdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Util
 open Names
@@ -46,14 +46,14 @@ let add dn (na,(pat,valu)) =
   let hkey = Option.map fst (Termdn.constr_pat_discr pat) in 
   dn.table <- Gmap.add na (pat,valu) dn.table;
   let dnm = dn.patterns in
-  dn.patterns <- Gmap.add hkey (Btermdn.add (get_dn dnm hkey) (pat,valu)) dnm
+  dn.patterns <- Gmap.add hkey (Btermdn.add None (get_dn dnm hkey) (pat,valu)) dnm
     
 let rmv dn na =
   let (pat,valu) = Gmap.find na dn.table in
   let hkey = Option.map fst (Termdn.constr_pat_discr pat) in 
   dn.table <- Gmap.remove na dn.table;
   let dnm = dn.patterns in
-  dn.patterns <- Gmap.add hkey (Btermdn.rmv (get_dn dnm hkey) (pat,valu)) dnm
+  dn.patterns <- Gmap.add hkey (Btermdn.rmv None (get_dn dnm hkey) (pat,valu)) dnm
 
 let in_dn dn na = Gmap.mem na dn.table
 			  
@@ -62,8 +62,12 @@ let remap ndn na (pat,valu) =
   add ndn (na,(pat,valu))
 
 let lookup dn valu =
-  let hkey = Option.map fst (Termdn.constr_val_discr valu) in 
-  try Btermdn.lookup (Gmap.find hkey  dn.patterns) valu with Not_found -> []
+  let hkey = 
+    match (Termdn.constr_val_discr valu) with 
+    | Dn.Label(l,_) -> Some l
+    | _ -> None
+  in 
+  try Btermdn.lookup None (Gmap.find hkey dn.patterns) valu with Not_found -> []
 
 let app f dn = Gmap.iter f dn.table