Removing useless uses of Gmap.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16520 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 3 insertions, 17 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ec9c0a95ee..8db7de46cb 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -145,8 +145,6 @@ let ppenv e = pp
 
 let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
 
-let ppinsts c = pp (pr_instance_gmap c)
-
 let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
 let cnt = ref 0
diff --git a/interp/notation.ml b/interp/notation.ml
index 80e23ce6a7..8ec5786219 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -955,10 +955,6 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
 
 let init () =
   init_scope_map ();
-(*
-  scope_stack := Gmap.empty
-  arguments_scope := Refmap.empty
-*)
   notation_level_map := String.Map.empty;
   delimiters_map := String.Map.empty;
   notations_key_table := KeyMap.empty;
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) =
diff --git a/printing/printer.ml b/printing/printer.ml
index 5d63d179db..696f25695b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -698,11 +698,6 @@ open Typeclasses
 let pr_instance i =
   pr_global (instance_impl i)
 
-let pr_instance_gmap insts =
-  prlist_with_sep fnl (fun (gr, insts) ->
-    prlist_with_sep fnl pr_instance (cmap_to_list insts))
-    (Gmap.to_list insts)
-
 (** Inductive declarations *)
 
 open Termops
diff --git a/printing/printer.mli b/printing/printer.mli
index fea8c06735..7c3a64b851 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -168,9 +168,6 @@ val set_printer_pr : printer_pr -> unit
 
 val default_printer_pr : printer_pr
 
-val pr_instance_gmap : (global_reference, Typeclasses.instance Names.Cmap.t) Gmap.t ->
-  Pp.std_ppcmds
-
 (** Inductive declarations *)
 
 val pr_mutual_inductive_body :