diff options
Diffstat (limited to 'tactics/nbtermdn.ml')
| -rw-r--r-- | tactics/nbtermdn.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index 0867d220..554ce2e9 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nbtermdn.ml 6427 2004-12-07 17:41:10Z sacerdot $ *) +(* $Id: nbtermdn.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Util open Names @@ -43,14 +43,14 @@ let get_dn dnm hkey = try Gmap.find hkey dnm with Not_found -> Btermdn.create () let add dn (na,(pat,valu)) = - let hkey = option_app fst (Termdn.constr_pat_discr pat) in + 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 let rmv dn na = let (pat,valu) = Gmap.find na dn.table in - let hkey = option_app fst (Termdn.constr_pat_discr pat) 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 @@ -62,7 +62,7 @@ let remap ndn na (pat,valu) = add ndn (na,(pat,valu)) let lookup dn valu = - let hkey = option_app fst (Termdn.constr_val_discr valu) in + let hkey = option_map fst (Termdn.constr_val_discr valu) in try Btermdn.lookup (Gmap.find hkey dn.patterns) valu with Not_found -> [] let app f dn = Gmap.iter f dn.table |