diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-14 08:59:15 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-14 08:59:15 +0000 |
| commit | f60fcb9ddae0c8df56a2d05233b48fccd7abe816 (patch) | |
| tree | 370ae8ae50428a93d806a912faddd42f3f5fcb24 /pretyping/term_dnet.ml | |
| parent | 12e1e2267dff48b13f4a8c3ef2527b2135698dbe (diff) | |
Removing useless uses of Gmap.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16520 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/term_dnet.ml')
| -rw-r--r-- | pretyping/term_dnet.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 862dbb4fa..79e61ecef 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -315,11 +315,11 @@ struct fold_pattern (fun acc (mset,m,dn) -> if Int.equal m neutral_meta then acc else f m dn acc) let fold_pattern_nonlin f = - let defined = ref Gmap.empty in + let defined = ref Int.Map.empty in fold_pattern_neutral ( fun m dn acc -> - let dn = try TDnet.inter dn (Gmap.find m !defined) with Not_found -> dn in - defined := Gmap.add m dn !defined; + let dn = try TDnet.inter dn (Int.Map.find m !defined) with Not_found -> dn in + defined := Int.Map.add m dn !defined; f m dn acc ) let fold_pattern_up f acc dpat cpat dn (up,plug) = |