diff options
| author | Pierre-Marie Pédrot | 2018-09-13 15:54:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-02 09:27:47 +0200 |
| commit | bc240341d9f0f7466c82e8ee9f3f325cda6fc3bf (patch) | |
| tree | 458d01bb58cbced90ce769eeb5a6eab15cbf6c3f /plugins | |
| parent | 1407a1caabd5891552043e9f62e5f2058df07034 (diff) | |
Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.
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 |