Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.

3 files changed, 4 insertions, 9 deletions

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
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 157f41bd7b..0e35583b14 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -167,11 +167,6 @@ Steps to perform:
 Handwritten classifiers declared through the `CLASSIFIED BY` statement are
 considered OCaml code, so they also need to be wrapped in braces.
 
-All extension macros are now behaving as if they were declared `FUNCTIONAL`,
-which means that they must return an interpretation state. This should
-currently be done by merely returning the `st` variable that is implicitly
-passed to the rule code.
-
 For instance, code of the form:
 ```
 VERNAC COMMAND EXTEND my_command CLASSIFIED BY classifier
@@ -182,8 +177,8 @@ END
 should be turned into
 ```
 VERNAC COMMAND EXTEND my_command CLASSIFIED BY { classifier }
-  [ "foo" int(i) ] => { classif' } -> { let () = cmd1 i in st }
-| [ "bar" ] -> { let () = cmd2 in st  }
+| [ "foo" int(i) ] => { classif' } -> { cmd1 i }
+| [ "bar" ] -> { cmd2 }
 END
 ```
 
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