diff options
| author | Emilio Jesus Gallego Arias | 2019-06-17 04:34:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-26 01:15:49 +0200 |
| commit | 81494db46137b2934167ae12d0b86e27e28023e9 (patch) | |
| tree | ad2a7b85cde2409debfd5f0650c3b70c467c7a7a /plugins/ltac | |
| parent | 2433d810b9850d25819f97643664a851d29d2e0f (diff) | |
[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.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |