From 245af3e197c36482931248479c8eca5d0e6459a6 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 25 Mar 2020 10:21:32 -0700
Subject: Doc_grammar: Update cmd:: and tacn:: constructs in .rsts Remove
 unneeded source and output files Move all commands under command NT Add a lot
 of edits for commands and tactics

---
 doc/sphinx/language/gallina-extensions.rst             | 2 +-
 doc/sphinx/language/gallina-specification-language.rst | 6 ++----
 2 files changed, 3 insertions(+), 5 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 2abf6d02d2..8fcbeea570 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -996,7 +996,7 @@ are now available through the dot notation.
    Including multiple modules is a single :cmd:`Include` is equivalent to including each module
    in a separate :cmd:`Include` command.
 
-.. cmd:: Include Type @module_type_inl {* <+ @module_type_inl }
+.. cmd:: Include Type {+<+ @module_type_inl }
 
    .. deprecated:: 8.3
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 12a9a30f3d..fe359a23a9 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1533,10 +1533,8 @@ Computations
    | delta {? @delta_flag }
    ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums }
    | @one_term {? at @occs_nums }
-   occs_nums ::= {+ @num_or_var }
-   | - @num_or_var {* @int_or_var }
-   num_or_var ::= @num
-   | @ident
+   occs_nums ::= {+ {| @num | @ident } }
+   | - {| @num | @ident } {* @int_or_var }
    int_or_var ::= @int
    | @ident
    unfold_occ ::= @smart_qualid {? at @occs_nums }
-- 
cgit v1.2.3