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.

---
 coqpp/coqpp_main.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'coqpp')

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 602620968d..89b4d340b2 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -306,7 +306,7 @@ let print_rule_classifier fmt r = match r.vernac_class with
 | Some f -> fprintf fmt "Some @[(fun %a-> %s)@]" print_binders r.vernac_toks f.code
 
 let print_body fmt r =
-  fprintf fmt "@[(fun %a~atts@ ~st@ -> %s)@]"
+  fprintf fmt "@[(fun %a~atts@ ~st@ -> let () = %s in st)@]"
     print_binders r.vernac_toks r.vernac_body.code
 
 let rec print_sig fmt = function
-- 
cgit v1.2.3