From 886e8b549c2267c8e2f125669ceed00ca3e0fdb5 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Wed, 10 Jan 2024 13:57:52 +0100 Subject: [PATCH] update common.edit_mlg and orderedGrammar --- doc/tools/docgram/common.edit_mlg | 3 --- doc/tools/docgram/orderedGrammar | 1 - 2 files changed, 4 deletions(-) diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a9227e1161ba4..025704edf66b8 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -744,9 +744,6 @@ gallina_ext: [ | REPLACE "Coercion" global OPT [ OPT univ_decl def_body ] | WITH "Coercion" ident_decl def_body -| REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type -| WITH "Include" "Type" LIST1 module_type_inl SEP "<+" - | REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] | WITH "Generalizable" [ [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 8d09b457752a4..25f2a1393cb74 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -938,7 +938,6 @@ command: [ | "Import" OPT import_categories LIST1 filtered_import | "Export" OPT import_categories LIST1 filtered_import | "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) -| "Include" "Type" LIST1 module_type_inl SEP "<+" | "Transparent" OPT "!" LIST1 reference | "Opaque" OPT "!" LIST1 reference | "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ]