aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools/docgram')
-rw-r--r--doc/tools/docgram/common.edit_mlg8
-rw-r--r--doc/tools/docgram/doc_grammar.ml19
-rw-r--r--doc/tools/docgram/dune2
-rw-r--r--doc/tools/docgram/fullGrammar52
-rw-r--r--doc/tools/docgram/orderedGrammar49
5 files changed, 64 insertions, 66 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a22f7ae9f3..1e9be8dded 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -396,8 +396,8 @@ operconstr0: [
(* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
| DELETE "{" binder_constr "}"
| REPLACE "{|" record_declaration bar_cbrace
-| WITH "{|" LIST0 field_def bar_cbrace
-| MOVETO term_record "{|" LIST0 field_def bar_cbrace
+| WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
+| MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
| MOVETO term_generalizing "`{" operconstr200 "}"
| MOVETO term_generalizing "`(" operconstr200 ")"
| MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
@@ -585,7 +585,7 @@ constructor_list_or_record_decl: [
record_fields: [
| REPLACE record_field ";" record_fields
-| WITH LIST0 record_field SEP ";"
+| WITH LIST0 record_field SEP ";" OPT ";"
| DELETE record_field
| DELETE (* empty *)
]
@@ -615,7 +615,7 @@ of_type_with_opt_coercion: [
]
of_type_with_opt_coercion: [
-| [ ":" | ":>" | ":>>" ] type
+| [ ":" | ":>" ] type
]
attribute_value: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 0ac652c0db..177abe53fc 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -909,14 +909,17 @@ let apply_splice g edit_map =
List.iter (fun b ->
let (nt0, prods0) = b in
let rec splice_loop nt prods cnt =
- let max_cnt = 10 in
- let (nt', prods') = edit_rule g edit_map nt prods in
- if cnt > max_cnt then
- error "Splice for '%s' not done after %d iterations\n" nt0 max_cnt;
- if nt' = nt && prods' = prods then
- (nt', prods')
- else
- splice_loop nt' prods' (cnt+1)
+ if cnt >= 10 then begin
+ error "Splice for '%s' not done after %d iterations. Current value is:\n" nt0 cnt;
+ List.iter (fun prod -> Printf.eprintf " %s\n" (prod_to_str prod)) prods;
+ (nt, prods)
+ end else begin
+ let (nt', prods') = edit_rule g edit_map nt prods in
+ if nt' = nt && prods' = prods then
+ (nt, prods)
+ else
+ splice_loop nt' prods' (cnt+1)
+ end
in
let (nt', prods') = splice_loop nt0 prods0 0 in
g_update_prods g nt' prods')
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index ba07e6df0d..2a7b283f55 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -24,7 +24,7 @@
(glob_files %{project_root}/plugins/nsatz/*.mlg)
(glob_files %{project_root}/plugins/omega/*.mlg)
(glob_files %{project_root}/plugins/rtauto/*.mlg)
- (glob_files %{project_root}/plugins/setoid_ring/*.mlg)
+ (glob_files %{project_root}/plugins/ring/*.mlg)
(glob_files %{project_root}/plugins/syntax/*.mlg)
(glob_files %{project_root}/user-contrib/Ltac2/*.mlg)
; Sphinx files
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 2ee8e4347e..73641976e3 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -685,10 +685,10 @@ command: [
| "Show" "Zify" "UnOpSpec" (* micromega plugin *)
| "Show" "Zify" "BinOpSpec" (* micromega plugin *)
| "Show" "Zify" "Spec" (* micromega plugin *)
-| "Add" "Ring" ident ":" constr OPT ring_mods (* setoid_ring plugin *)
-| "Print" "Rings" (* setoid_ring plugin *)
-| "Add" "Field" ident ":" constr OPT field_mods (* setoid_ring plugin *)
-| "Print" "Fields" (* setoid_ring plugin *)
+| "Add" "Ring" ident ":" constr OPT ring_mods (* ring plugin *)
+| "Print" "Rings" (* ring plugin *)
+| "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *)
+| "Print" "Fields" (* ring plugin *)
| "Number" "Notation" reference reference reference ":" ident numnotoption
| "Numeral" "Notation" reference reference reference ":" ident numnotoption
| "String" "Notation" reference reference reference ":" ident
@@ -986,10 +986,7 @@ constructor: [
]
of_type_with_opt_coercion: [
-| ":>>"
-| ":>" ">"
| ":>"
-| ":" ">" ">"
| ":" ">"
| ":"
]
@@ -1743,11 +1740,11 @@ simple_tactic: [
| "zify_elim_let" (* micromega plugin *)
| "nsatz_compute" constr (* nsatz plugin *)
| "omega" (* omega plugin *)
+| "protect_fv" string "in" ident (* ring plugin *)
+| "protect_fv" string (* ring plugin *)
+| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *)
+| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* ring plugin *)
| "rtauto"
-| "protect_fv" string "in" ident (* setoid_ring plugin *)
-| "protect_fv" string (* setoid_ring plugin *)
-| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *)
-| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *)
]
mlname: [
@@ -1761,7 +1758,6 @@ int_or_id: [
]
language: [
-| "Ocaml" (* extraction plugin *)
| "OCaml" (* extraction plugin *)
| "Haskell" (* extraction plugin *)
| "Scheme" (* extraction plugin *)
@@ -2532,31 +2528,31 @@ induction_clause_list: [
]
ring_mod: [
-| "decidable" constr (* setoid_ring plugin *)
-| "abstract" (* setoid_ring plugin *)
-| "morphism" constr (* setoid_ring plugin *)
-| "constants" "[" tactic "]" (* setoid_ring plugin *)
-| "closed" "[" LIST1 global "]" (* setoid_ring plugin *)
-| "preprocess" "[" tactic "]" (* setoid_ring plugin *)
-| "postprocess" "[" tactic "]" (* setoid_ring plugin *)
-| "setoid" constr constr (* setoid_ring plugin *)
-| "sign" constr (* setoid_ring plugin *)
-| "power" constr "[" LIST1 global "]" (* setoid_ring plugin *)
-| "power_tac" constr "[" tactic "]" (* setoid_ring plugin *)
-| "div" constr (* setoid_ring plugin *)
+| "decidable" constr (* ring plugin *)
+| "abstract" (* ring plugin *)
+| "morphism" constr (* ring plugin *)
+| "constants" "[" tactic "]" (* ring plugin *)
+| "closed" "[" LIST1 global "]" (* ring plugin *)
+| "preprocess" "[" tactic "]" (* ring plugin *)
+| "postprocess" "[" tactic "]" (* ring plugin *)
+| "setoid" constr constr (* ring plugin *)
+| "sign" constr (* ring plugin *)
+| "power" constr "[" LIST1 global "]" (* ring plugin *)
+| "power_tac" constr "[" tactic "]" (* ring plugin *)
+| "div" constr (* ring plugin *)
]
ring_mods: [
-| "(" LIST1 ring_mod SEP "," ")" (* setoid_ring plugin *)
+| "(" LIST1 ring_mod SEP "," ")" (* ring plugin *)
]
field_mod: [
-| ring_mod (* setoid_ring plugin *)
-| "completeness" constr (* setoid_ring plugin *)
+| ring_mod (* ring plugin *)
+| "completeness" constr (* ring plugin *)
]
field_mods: [
-| "(" LIST1 field_mod SEP "," ")" (* setoid_ring plugin *)
+| "(" LIST1 field_mod SEP "," ")" (* ring plugin *)
]
numnotoption: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index aae96fc966..61befe9f1f 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -114,7 +114,7 @@ ident_decl: [
]
of_type: [
-| [ ":" | ":>" | ":>>" ] type
+| [ ":" | ":>" ] type
]
qualid: [
@@ -539,7 +539,7 @@ variant_definition: [
]
record_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations
+| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" OPT decl_notations
]
record_field: [
@@ -553,7 +553,7 @@ field_body: [
]
term_record: [
-| "{|" LIST0 field_def "|}"
+| "{|" LIST0 field_def SEP ";" OPT ";" "|}"
]
field_def: [
@@ -566,7 +566,7 @@ inductive_definition: [
constructors_or_record: [
| OPT "|" LIST1 constructor SEP "|"
-| OPT ident "{" LIST0 record_field SEP ";" "}"
+| OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}"
]
constructor: [
@@ -892,10 +892,10 @@ command: [
| "Show" "Zify" "UnOpSpec" (* micromega plugin *)
| "Show" "Zify" "BinOpSpec" (* micromega plugin *)
| "Show" "Zify" "Spec" (* micromega plugin *)
-| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* setoid_ring plugin *)
-| "Print" "Rings" (* setoid_ring plugin *)
-| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *)
-| "Print" "Fields" (* setoid_ring plugin *)
+| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* ring plugin *)
+| "Print" "Rings" (* ring plugin *)
+| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *)
+| "Print" "Fields" (* ring plugin *)
| "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier
| "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
| "Typeclasses" "Transparent" LIST0 qualid
@@ -1268,7 +1268,6 @@ int_or_id: [
]
language: [
-| "Ocaml" (* extraction plugin *)
| "OCaml" (* extraction plugin *)
| "Haskell" (* extraction plugin *)
| "Scheme" (* extraction plugin *)
@@ -1280,23 +1279,23 @@ fun_scheme_arg: [
]
ring_mod: [
-| "decidable" one_term (* setoid_ring plugin *)
-| "abstract" (* setoid_ring plugin *)
-| "morphism" one_term (* setoid_ring plugin *)
-| "constants" "[" ltac_expr "]" (* setoid_ring plugin *)
-| "preprocess" "[" ltac_expr "]" (* setoid_ring plugin *)
-| "postprocess" "[" ltac_expr "]" (* setoid_ring plugin *)
-| "setoid" one_term one_term (* setoid_ring plugin *)
-| "sign" one_term (* setoid_ring plugin *)
-| "power" one_term "[" LIST1 qualid "]" (* setoid_ring plugin *)
-| "power_tac" one_term "[" ltac_expr "]" (* setoid_ring plugin *)
-| "div" one_term (* setoid_ring plugin *)
-| "closed" "[" LIST1 qualid "]" (* setoid_ring plugin *)
+| "decidable" one_term (* ring plugin *)
+| "abstract" (* ring plugin *)
+| "morphism" one_term (* ring plugin *)
+| "constants" "[" ltac_expr "]" (* ring plugin *)
+| "preprocess" "[" ltac_expr "]" (* ring plugin *)
+| "postprocess" "[" ltac_expr "]" (* ring plugin *)
+| "setoid" one_term one_term (* ring plugin *)
+| "sign" one_term (* ring plugin *)
+| "power" one_term "[" LIST1 qualid "]" (* ring plugin *)
+| "power_tac" one_term "[" ltac_expr "]" (* ring plugin *)
+| "div" one_term (* ring plugin *)
+| "closed" "[" LIST1 qualid "]" (* ring plugin *)
]
field_mod: [
-| ring_mod (* setoid_ring plugin *)
-| "completeness" one_term (* setoid_ring plugin *)
+| ring_mod (* ring plugin *)
+| "completeness" one_term (* ring plugin *)
]
numeral_modifier: [
@@ -1642,8 +1641,8 @@ simple_tactic: [
| "nsatz_compute" one_term (* nsatz plugin *)
| "omega" (* omega plugin *)
| "protect_fv" string OPT ( "in" ident )
-| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *)
-| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *)
+| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *)
+| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *)
| match_key OPT "reverse" "goal" "with" OPT "|" LIST1 ( goal_pattern "=>" ltac_expr ) SEP "|" "end"
| match_key ltac_expr "with" OPT "|" LIST1 ( match_pattern "=>" ltac_expr ) SEP "|" "end"
| "classical_left"
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 00:58:09 +0000