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
---
 interp/notation.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'interp/notation.ml')

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;
-- 
cgit v1.2.3