3 files changed, 3 insertions, 8 deletions
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index fba4856241..a533a6d367 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -43,9 +43,6 @@
   orderedGrammar)
  (action
   (progn
-   (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.old; done")
-   (chdir %{project_root} (run doc_grammar -check-cmds %{input}))
-   (bash "for f in fullGrammar orderedGrammar; do cp ${f} ${f}.new; done")
-   (bash "for f in fullGrammar orderedGrammar; do cp ${f}.old ${f}; done")
+   (chdir %{project_root} (run doc_grammar -check-cmds -no-update %{input}))
    (diff? fullGrammar fullGrammar.new)
    (diff? orderedGrammar orderedGrammar.new))))
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 272d17bb35..dc7e0fba37 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -773,7 +773,7 @@ gallina: [
 | assumption_token inline assum_list
 | assumptions_token inline assum_list
 | def_token ident_decl def_body
-| "Let" identref def_body
+| "Let" ident_decl def_body
 | finite_token LIST1 inductive_definition SEP "with"
 | "Fixpoint" LIST1 rec_definition SEP "with"
 | "Let" "Fixpoint" LIST1 rec_definition SEP "with"
@@ -1027,7 +1027,6 @@ gallina_ext: [
 | "Module" "Type" identref LIST0 module_binder check_module_types is_module_type
 | "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl
 | "Section" identref
-| "Chapter" identref
 | "End" identref
 | "Collection" identref ":=" section_subset_expr
 | "Require" export_token LIST1 global
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 0c9d7a853b..535976b7d9 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -851,7 +851,7 @@ command: [
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
 | assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
 | [ "Definition" | "Example" ] ident_decl def_body
-| "Let" ident def_body
+| "Let" ident_decl def_body
 | "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
 | "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
 | "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition )
@@ -873,7 +873,6 @@ command: [
 | "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" )
 | "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl
 | "Section" ident
-| "Chapter" ident
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid