diff options
| author | Maxime Dénès | 2019-02-26 10:19:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-26 10:19:18 +0100 |
| commit | 3459155e1c629a2f932c4d4d917b0f69aa89ccf7 (patch) | |
| tree | 8f1db2c3e2a0d89a412c9c19b6ca458160f4c6c4 /vernac/class.ml | |
| parent | fc76c77ac6e509c1bccc2823ce2037d21a53276a (diff) | |
| parent | d31056ec924ef6e09b28bc3822b427b67a8a300b (diff) | |
Merge PR #9567: [vernac] Unify declaration hooks.
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: maximedenes
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 |