diff options
Diffstat (limited to 'tactics/nbtermdn.ml')
| -rw-r--r-- | tactics/nbtermdn.ml | 14 |
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 |