diff options
Diffstat (limited to 'tactics/nbtermdn.ml')
| -rw-r--r-- | tactics/nbtermdn.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index d53ca6126..c53a5088a 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -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_map 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_map 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_map 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 |