diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg
index 9100e7fea..4c7c8e4fc 100644
--- a/src/coq_elpi_vernacular_syntax.mlg
+++ b/src/coq_elpi_vernacular_syntax.mlg
@@ -231,9 +231,12 @@ VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([
 | #[ atts = any_attribute ] [ "Elpi" "Query"  qualified_name(p) elpi_string(s) ] -> {
      let () = ignore_unknown_attributes atts in
      EV.run_in_program ~program:(snd p) s }
-| #[ atts = any_attribute ] [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } -> {
-     let () = ignore_unknown_attributes atts in
-     EV.export_command (snd p) }
+| #[ atts = any_attribute ] [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } SYNTERP AS _ {
+     EV.export_command (snd p)
+  } -> {
+     let () = ignore_unknown_attributes atts in  
+     ()
+  }
 | #[ atts = any_attribute ] [ "Elpi" qualified_name(p) elpi_cmd_arg_list(args) ] -> {
      EV.run_program (fst p) (snd p) ~atts args }
 END