From bc240341d9f0f7466c82e8ee9f3f325cda6fc3bf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 13 Sep 2018 15:54:08 +0200
Subject: Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.

---
 plugins/derive/g_derive.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3