aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools')
-rw-r--r--doc/tools/coqrst/coqdomain.py31
-rw-r--r--doc/tools/docgram/common.edit_mlg43
-rw-r--r--doc/tools/docgram/fullGrammar11
-rw-r--r--doc/tools/docgram/orderedGrammar78
4 files changed, 103 insertions, 60 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index fa739e97bc..1428dae7ef 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -529,12 +529,12 @@ class ProductionObject(CoqObject):
self.signatures = []
indexnode = super().run()[0] # makes calls to handle_signature
- table = nodes.container(classes=['prodn-table'])
- tgroup = nodes.container(classes=['prodn-column-group'])
+ table = nodes.inline(classes=['prodn-table'])
+ tgroup = nodes.inline(classes=['prodn-column-group'])
for _ in range(4):
- tgroup += nodes.container(classes=['prodn-column'])
+ tgroup += nodes.inline(classes=['prodn-column'])
table += tgroup
- tbody = nodes.container(classes=['prodn-row-group'])
+ tbody = nodes.inline(classes=['prodn-row-group'])
table += tbody
# create rows
@@ -542,8 +542,8 @@ class ProductionObject(CoqObject):
lhs, op, rhs, tag = signature
position = self.state_machine.get_source_and_line(self.lineno)
- row = nodes.container(classes=['prodn-row'])
- entry = nodes.container(classes=['prodn-cell-nonterminal'])
+ row = nodes.inline(classes=['prodn-row'])
+ entry = nodes.inline(classes=['prodn-cell-nonterminal'])
if lhs != "":
target_name = make_id('grammar-token-' + lhs)
target = nodes.target('', '', ids=[target_name], names=[target_name])
@@ -553,19 +553,19 @@ class ProductionObject(CoqObject):
entry += inline
entry += notation_to_sphinx('@'+lhs, *position)
else:
- entry += nodes.Text('')
+ entry += nodes.literal('', '')
row += entry
- entry = nodes.container(classes=['prodn-cell-op'])
- entry += nodes.Text(op)
+ entry = nodes.inline(classes=['prodn-cell-op'])
+ entry += nodes.literal(op, op)
row += entry
- entry = nodes.container(classes=['prodn-cell-production'])
+ entry = nodes.inline(classes=['prodn-cell-production'])
entry += notation_to_sphinx(rhs, *position)
row += entry
- entry = nodes.container(classes=['prodn-cell-tag'])
- entry += nodes.Text(tag)
+ entry = nodes.inline(classes=['prodn-cell-tag'])
+ entry += nodes.literal(tag, tag)
row += entry
tbody += row
@@ -1171,9 +1171,12 @@ class StdGlossaryIndex(Index):
name, localname, shortname = "glossindex", "Glossary", "terms"
def generate(self, docnames=None):
- content = defaultdict(list)
+ def ci_sort(entry):
+ ((type, itemname), (docname, anchor)) = entry
+ return itemname.lower()
- for ((type, itemname), (docname, anchor)) in self.domain.data['objects'].items():
+ content = defaultdict(list)
+ for ((type, itemname), (docname, anchor)) in sorted(self.domain.data['objects'].items(), key=ci_sort):
if type == 'term':
entries = content[itemname[0].lower()]
entries.append([itemname, 0, docname, anchor, '', '', ''])
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 27144fd1ad..fd1c3c0260 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -62,8 +62,8 @@ SPLICE: [
]
RENAME: [
-| G_LTAC2_delta_flag ltac2_delta_flag
-| G_LTAC2_strategy_flag ltac2_strategy_flag
+| G_LTAC2_delta_flag ltac2_delta_reductions
+| G_LTAC2_strategy_flag ltac2_reductions
| G_LTAC2_binder ltac2_binder
| G_LTAC2_branches ltac2_branches
| G_LTAC2_let_clause ltac2_let_clause
@@ -640,7 +640,7 @@ delta_flag: [
| OPTINREF
]
-ltac2_delta_flag: [
+ltac2_delta_reductions: [
| EDIT ADD_OPT "-" "[" refglobals "]" (* Ltac2 plugin *)
]
@@ -924,6 +924,10 @@ where: [
| "before" ident
]
+simple_occurrences: [
+(* placeholder (yuck) *)
+]
+
simple_tactic: [
| REPLACE "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
| WITH "eauto" OPT nat_or_var auto_using hintbases
@@ -937,6 +941,26 @@ simple_tactic: [
| DELETE "autorewrite" "*" "with" LIST1 preident clause
| REPLACE "autorewrite" "*" "with" LIST1 preident clause "using" tactic
| WITH "autorewrite" OPT "*" "with" LIST1 preident clause OPT ( "using" tactic )
+| REPLACE "autounfold" hintbases clause_dft_concl
+| WITH "autounfold" hintbases OPT simple_occurrences
+| REPLACE "red" clause_dft_concl
+| WITH "red" simple_occurrences
+| REPLACE "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl
+| WITH "simpl" OPT delta_flag OPT ref_or_pattern_occ simple_occurrences
+| REPLACE "hnf" clause_dft_concl
+| WITH "hnf" simple_occurrences
+| REPLACE "cbv" strategy_flag clause_dft_concl
+| WITH "cbv" strategy_flag simple_occurrences
+| PRINT
+| REPLACE "compute" OPT delta_flag clause_dft_concl
+| WITH "compute" OPT delta_flag simple_occurrences
+| REPLACE "lazy" strategy_flag clause_dft_concl
+| WITH "lazy" strategy_flag simple_occurrences
+| REPLACE "cbn" strategy_flag clause_dft_concl
+| WITH "cbn" strategy_flag simple_occurrences
+| REPLACE "fold" LIST1 constr clause_dft_concl
+| WITH "fold" LIST1 constr simple_occurrences
+
| DELETE "cofix" ident
| REPLACE "cofix" ident "with" LIST1 cofixdecl
| WITH "cofix" ident OPT ( "with" LIST1 cofixdecl )
@@ -2460,6 +2484,10 @@ clause_dft_concl: [
| WITH occs
]
+simple_occurrences: [
+| clause_dft_concl (* semantically restricted: no "at" clause *)
+]
+
occs_nums: [
| EDIT ADD_OPT "-" LIST1 nat_or_var
]
@@ -2471,10 +2499,8 @@ variance_identref: [
conversion: [
| DELETE constr
| DELETE constr "with" constr
-| PRINT
| REPLACE constr "at" occs_nums "with" constr
| WITH OPT ( constr OPT ( "at" occs_nums ) "with" ) constr
-| PRINT
]
SPLICE: [
@@ -2704,6 +2730,7 @@ SPLICE: [
| variance_identref
| rewriter
| conversion
+| type_cast
] (* end SPLICE *)
RENAME: [
@@ -2762,6 +2789,10 @@ RENAME: [
| hypident_occ hyp_occs
| concl_occ concl_occs
| constr_with_bindings_arg one_term_with_bindings
+| red_flag reduction
+| strategy_flag reductions
+| delta_flag delta_reductions
+| q_strategy_flag q_reductions
]
simple_tactic: [
@@ -2806,7 +2837,7 @@ NOTINRSTS: [
| q_destruction_arg
| q_with_bindings
| q_bindings
-| q_strategy_flag
+| q_reductions
| q_reference
| q_clause
| q_occurrences
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index bc6b803bbb..ab1a9d4c75 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -3283,7 +3283,7 @@ ltac2_expr6: [
]
ltac2_expr5: [
-| "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6 (* Ltac2 plugin *)
+| "fun" LIST1 G_LTAC2_input_fun type_cast "=>" ltac2_expr6 (* Ltac2 plugin *)
| "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6 (* Ltac2 plugin *)
| "match" ltac2_expr5 "with" G_LTAC2_branches "end" (* Ltac2 plugin *)
| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5 (* Ltac2 plugin *)
@@ -3371,8 +3371,13 @@ tac2expr_in_env: [
| ltac2_expr6 (* Ltac2 plugin *)
]
+type_cast: [
+| (* Ltac2 plugin *)
+| ":" ltac2_type5 (* Ltac2 plugin *)
+]
+
G_LTAC2_let_clause: [
-| let_binder ":=" ltac2_expr6 (* Ltac2 plugin *)
+| let_binder type_cast ":=" ltac2_expr6 (* Ltac2 plugin *)
]
let_binder: [
@@ -3415,7 +3420,7 @@ G_LTAC2_input_fun: [
]
tac2def_body: [
-| G_LTAC2_binder LIST0 G_LTAC2_input_fun ":=" ltac2_expr6 (* Ltac2 plugin *)
+| G_LTAC2_binder LIST0 G_LTAC2_input_fun type_cast ":=" ltac2_expr6 (* Ltac2 plugin *)
]
tac2def_val: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index a34e96ac16..5b19b7fc55 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -337,7 +337,7 @@ NOTINRSTS: [
| q_destruction_arg
| q_with_bindings
| q_bindings
-| q_strategy_flag
+| q_reductions
| q_reference
| q_clause
| q_occurrences
@@ -550,9 +550,9 @@ term_generalizing: [
]
term_cast: [
+| term10 ":" type
| term10 "<:" type
| term10 "<<:" type
-| term10 ":" type
| term10 ":>"
]
@@ -627,38 +627,38 @@ reduce: [
]
red_expr: [
-| "red"
-| "hnf"
-| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ]
-| "cbv" OPT strategy_flag
-| "cbn" OPT strategy_flag
-| "lazy" OPT strategy_flag
-| "compute" OPT delta_flag
+| "lazy" OPT reductions
+| "cbv" OPT reductions
+| "compute" OPT delta_reductions
| "vm_compute" OPT [ reference_occs | pattern_occs ]
| "native_compute" OPT [ reference_occs | pattern_occs ]
+| "red"
+| "hnf"
+| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ]
+| "cbn" OPT reductions
| "unfold" LIST1 reference_occs SEP ","
| "fold" LIST1 one_term
| "pattern" LIST1 pattern_occs SEP ","
| ident
]
-delta_flag: [
-| OPT "-" "[" LIST1 reference "]"
-]
-
-strategy_flag: [
-| LIST1 red_flag
-| delta_flag
+reductions: [
+| LIST1 reduction
+| delta_reductions
]
-red_flag: [
+reduction: [
| "beta"
-| "iota"
+| "delta" OPT delta_reductions
| "match"
| "fix"
| "cofix"
+| "iota"
| "zeta"
-| "delta" OPT delta_flag
+]
+
+delta_reductions: [
+| OPT "-" "[" LIST1 reference "]"
]
reference_occs: [
@@ -1242,6 +1242,10 @@ occurrences: [
| "in" goal_occurrences
]
+simple_occurrences: [
+| occurrences
+]
+
occs_nums: [
| OPT "-" LIST1 nat_or_var
]
@@ -1741,7 +1745,7 @@ simple_tactic: [
| "info_eauto" OPT nat_or_var OPT auto_using OPT hintbases
| "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
| "bfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
-| "autounfold" OPT hintbases OPT occurrences
+| "autounfold" OPT hintbases OPT simple_occurrences
| "autounfold_one" OPT hintbases OPT ( "in" ident )
| "unify" one_term one_term OPT ( "with" ident )
| "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident )
@@ -1811,17 +1815,17 @@ simple_tactic: [
| "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
| "inversion_clear" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
| "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident )
-| "red" OPT occurrences
-| "hnf" OPT occurrences
-| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ] OPT occurrences
-| "cbv" OPT strategy_flag OPT occurrences
-| "cbn" OPT strategy_flag OPT occurrences
-| "lazy" OPT strategy_flag OPT occurrences
-| "compute" OPT delta_flag OPT occurrences
+| "red" simple_occurrences
+| "hnf" simple_occurrences
+| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ] simple_occurrences
+| "cbv" OPT reductions simple_occurrences
+| "cbn" OPT reductions simple_occurrences
+| "lazy" OPT reductions simple_occurrences
+| "compute" OPT delta_reductions simple_occurrences
| "vm_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences
| "native_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences
| "unfold" LIST1 reference_occs SEP "," OPT occurrences
-| "fold" LIST1 one_term OPT occurrences
+| "fold" LIST1 one_term simple_occurrences
| "pattern" LIST1 pattern_occs SEP "," OPT occurrences
| "change" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences
| "change_no_check" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences
@@ -2139,13 +2143,13 @@ ltac2_goal_tactics: [
| LIST0 ( OPT ltac2_expr ) SEP "|" (* Ltac2 plugin *)
]
-q_strategy_flag: [
-| ltac2_strategy_flag (* Ltac2 plugin *)
+q_reductions: [
+| ltac2_reductions (* Ltac2 plugin *)
]
-ltac2_strategy_flag: [
+ltac2_reductions: [
| LIST1 ltac2_red_flag (* Ltac2 plugin *)
-| OPT ltac2_delta_flag (* Ltac2 plugin *)
+| OPT ltac2_delta_reductions (* Ltac2 plugin *)
]
ltac2_red_flag: [
@@ -2155,10 +2159,10 @@ ltac2_red_flag: [
| "fix" (* Ltac2 plugin *)
| "cofix" (* Ltac2 plugin *)
| "zeta" (* Ltac2 plugin *)
-| "delta" OPT ltac2_delta_flag (* Ltac2 plugin *)
+| "delta" OPT ltac2_delta_reductions (* Ltac2 plugin *)
]
-ltac2_delta_flag: [
+ltac2_delta_reductions: [
| OPT "-" "[" LIST1 refglobal "]"
]
@@ -2270,7 +2274,7 @@ ltac2_entry: [
]
tac2def_body: [
-| [ "_" | ident ] LIST0 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *)
+| [ "_" | ident ] LIST0 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr (* Ltac2 plugin *)
]
tac2typ_def: [
@@ -2311,13 +2315,13 @@ ltac2_expr: [
]
ltac2_expr5: [
-| "fun" LIST1 tac2pat0 "=>" ltac2_expr (* Ltac2 plugin *)
+| "fun" LIST1 tac2pat0 OPT ( ":" ltac2_type ) "=>" ltac2_expr (* Ltac2 plugin *)
| "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr (* Ltac2 plugin *)
| ltac2_expr3 (* Ltac2 plugin *)
]
ltac2_let_clause: [
-| LIST1 tac2pat0 ":=" ltac2_expr (* Ltac2 plugin *)
+| LIST1 tac2pat0 OPT ( ":" ltac2_type ) ":=" ltac2_expr (* Ltac2 plugin *)
]
ltac2_expr3: [
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 00:15:15 +0000