aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/declarations.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-02 22:08:28 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-02 22:08:28 +0000
commit42cbb18f5b0e220a832ccf5db320d90be5ce0c8e (patch)
treee009842c2be91301343ac1fe23e54b7480ff6736 /checker/declarations.ml
parent8211140b73a3e1132ab70d8d75d4debc6e48ea4f (diff)
Minor cleanup concerning Mod_subst.MBImap
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16380 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/declarations.ml')
-rw-r--r--checker/declarations.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 69dd26130..335aba520 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -59,12 +59,6 @@ type delta_resolver = Deltamap.t
let empty_delta_resolver = Deltamap.empty
-module MBImap = Map.Make
- (struct
- type t = MBId.t
- let compare = Pervasives.compare
- end)
-
module Umap = struct
type 'a t = 'a MPmap.t * 'a MBImap.t
let empty = MPmap.empty, MBImap.empty