diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 22:37:33 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-23 16:53:53 +0100 |
| commit | d31056ec924ef6e09b28bc3822b427b67a8a300b (patch) | |
| tree | d720333732d9be1a03f74cc079e0a1903d31e023 /vernac/class.ml | |
| parent | c37e90b67c74b32837409a9a424757246067ef1b (diff) | |
[vernac] Unify declaration hooks.
Supersedes #8718.
Diffstat (limited to 'vernac/class.ml')
| -rw-r--r-- | vernac/class.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |