From c8883873426c92778a1cac02da17e3d123beb394 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 10 Oct 2018 23:35:47 +0200
Subject: [vernac] Remove unused abstraction from declaration_hook type.

"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.

We thus remove the polymorphism with the hope to be able to reify the
control later on.
---
 vernac/class.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/class.mli')

diff --git a/vernac/class.mli b/vernac/class.mli
index f7e837f3bb..80d6d4383c 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
 val try_add_new_identity_coercion : Id.t -> local:bool -> 
   Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
 
-val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
 
 val class_of_global : GlobRef.t -> cl_typ
-- 
cgit v1.2.3