From 74ddca99c649f2f8c203582a9b82bddf64fb6b52 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Apr 2014 15:31:12 +0200
Subject: Removing dead code, thanks to new OCaml warnings and a bit of
 scripting.

---
 library/global.ml     | 1 -
 library/globnames.mli | 2 ++
 library/nametab.ml    | 4 ----
 library/nametab.mli   | 2 --
 4 files changed, 2 insertions(+), 7 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 9f683b2ff1..a8121d15f2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 
 (** We introduce here the global environment of the system,
diff --git a/library/globnames.mli b/library/globnames.mli
index 0a7bf850c0..5d717965e9 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -49,12 +49,14 @@ val reference_of_constr : constr -> global_reference
 module RefOrdered : sig
   type t = global_reference
   val compare : t -> t -> int
+  val equal : t -> t -> bool
   val hash : t -> int
 end
 
 module RefOrdered_env : sig
   type t = global_reference
   val compare : t -> t -> int
+  val equal : t -> t -> bool
   val hash : t -> int
 end
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 03856736da..1a30e80d13 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -15,14 +15,10 @@ open Globnames
 
 
 exception GlobalizationError of qualid
-exception GlobalizationConstantError of qualid
 
 let error_global_not_found_loc loc q =
   Loc.raise loc (GlobalizationError q)
 
-let error_global_constant_not_found_loc loc q =
-  Loc.raise loc (GlobalizationConstantError q)
-
 let error_global_not_found q = raise (GlobalizationError q)
 
 (* Kinds of global names *)
diff --git a/library/nametab.mli b/library/nametab.mli
index 43c174f1be..d9038c7741 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -58,12 +58,10 @@ open Globnames
 
 
 exception GlobalizationError of qualid
-exception GlobalizationConstantError of qualid
 
 (** Raises a globalization error *)
 val error_global_not_found_loc : Loc.t -> qualid -> 'a
 val error_global_not_found     : qualid -> 'a
-val error_global_constant_not_found_loc : Loc.t -> qualid -> 'a
 
 (** {6 Register visibility of things } *)
 
-- 
cgit v1.2.3