From d31056ec924ef6e09b28bc3822b427b67a8a300b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 22:37:33 +0100
Subject: [vernac] Unify declaration hooks.

Supersedes #8718.
---
 vernac/class.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/class.ml')

diff --git a/vernac/class.ml b/vernac/class.ml
index 823177d4d1..a6b3242cae 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -302,7 +302,7 @@ let try_add_new_identity_coercion id ~local poly ~source ~target =
 let try_add_new_coercion_with_source ref ~local poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
-let add_coercion_hook poly local ref =
+let add_coercion_hook poly _uctx _trans local ref =
   let local = match local with
   | Discharge
   | Local -> true
@@ -314,7 +314,7 @@ let add_coercion_hook poly local ref =
 
 let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
 
-let add_subclass_hook poly local ref =
+let add_subclass_hook poly _uctx _trans local ref =
   let stre = match local with
   | Local -> true
   | Global -> false
-- 
cgit v1.2.3