From 74c29764359272b29af081b30762549777ae8825 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sat, 2 Jan 2016 17:05:03 +0100
Subject: Remove some useless type declarations.

---
 ide/ideutils.ml    | 2 --
 ide/wg_Find.ml     | 2 --
 library/declare.ml | 3 ---
 library/keys.ml    | 2 --
 parsing/egramml.ml | 2 +-
 5 files changed, 1 insertion(+), 10 deletions(-)

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index ffa07ead7..51ae76ff5 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -9,8 +9,6 @@
 
 open Preferences
 
-exception Forbidden
-
 let warn_image () =
   let img = GMisc.image () in
   img#set_stock `DIALOG_WARNING;
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index a0949ca0c..dc7071c27 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type mode = [ `FIND | `REPLACE ]
-
 let b2c = Ideutils.byte_offset_to_char_offset
 
 class finder name (view : GText.view) =
diff --git a/library/declare.ml b/library/declare.ml
index 994a6557a..c1697a434 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -417,9 +417,6 @@ let assumption_message id =
 
 (** Global universe names, in a different summary *)
 
-type universe_names =
-    (Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
-
 (* Discharged or not *)
 type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
 
diff --git a/library/keys.ml b/library/keys.ml
index 3d277476f..6b2466f3d 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -62,8 +62,6 @@ module Keyset = Keymap.Set
 
 (* Mapping structure for references to be considered equivalent *)
 
-type keys = Keyset.t Keymap.t
-
 let keys = Summary.ref Keymap.empty ~name:"Keys_decl"
 
 let add_kv k v m =
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index e95b85bc2..9a380822e 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -49,7 +49,7 @@ let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = func
 
 type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
 
-let rec ty_eval : type s a r. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
+let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
 | TyStop -> fun f loc -> f loc []
 | TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f
 | TyNext (rem, tok, Some inj) -> fun f x ->
-- 
cgit v1.2.3