From f60fcb9ddae0c8df56a2d05233b48fccd7abe816 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 14 May 2013 08:59:15 +0000
Subject: Removing useless uses of Gmap.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16520 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/term_dnet.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 862dbb4fa3..79e61ecef1 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) =
-- 
cgit v1.2.3