From 81494db46137b2934167ae12d0b86e27e28023e9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 17 Jun 2019 04:34:06 +0200
Subject: [declare] Fine tuning of Hook type.

We turn the hook parameter into a record, making more explicit the
capture of data in hooks as they only take one parameter now

This is a fine-tuning but provides some small advantages, and allows
us to tweak the hook type with less breakage.
---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8acb29ba74..19866df8e3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1997,7 +1997,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let poly = atts.polymorphic in
   let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-  let hook _ _ _ = function
+  let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
     | Globnames.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info
-- 
cgit v1.2.3