diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/derive/g_derive.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 2e059c7f95..18316bf2cd 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuara VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } | [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { let () = Derive.start_deriving f suchthat lemma in st } + { Derive.start_deriving f suchthat lemma } END |