update common.edit_mlg and orderedGrammar

Villetaneuse · May 16, 2024 · 886e8b5 · 886e8b5
1 parent 7f45ee7
commit 886e8b5
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 4 deletions.
diff --git 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
@@ -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 "]" ]