Merge PR #13141: Document the removal of forward class hints.

Reviewed-by: jfehrle
Ack-by: ppedrot

5 files changed, 52 insertions, 50 deletions

diff --git a/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst b/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst
new file mode 100644
index 0000000000..7fe69c39c1
--- /dev/null
+++ b/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  Undocumented and experimental forward class hint feature ``:>>``.
+  Use ``:>`` (see :n:`@of_type`) instead
+  (`#13106 <https://github.com/coq/coq/pull/13106>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index fe10e345cd..41e1c30f0d 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -138,7 +138,7 @@ has type :n:`@type`.
       | {| Variable | Variables }
       assumpt ::= {+ @ident_decl } @of_type
       ident_decl ::= @ident {? @univ_decl }
-      of_type ::= {| : | :> | :>> } @type
+      of_type ::= {| : | :> } @type
 
    These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in
    the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a22f7ae9f3..a9f9c805d8 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -615,7 +615,7 @@ of_type_with_opt_coercion: [
 ]
 
 of_type_with_opt_coercion: [
-| [ ":" | ":>" | ":>>" ] type
+| [ ":" | ":>" ] type
 ]
 
 attribute_value: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 328175e65c..067050b4f5 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: [
-| ":>>"
-| ":>" ">"
 | ":>"
-| ":" ">" ">"
 | ":" ">"
 | ":"
 ]
@@ -1744,10 +1741,10 @@ simple_tactic: [
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega 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 *)
+| "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 *)
 ]
 
 mlname: [
@@ -2531,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 6ae99880b3..cbef29fb39 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -114,7 +114,7 @@ ident_decl: [
 ]
 
 of_type: [
-| [ ":" | ":>" | ":>>" ] type
+| [ ":" | ":>" ] type
 ]
 
 qualid: [
@@ -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
@@ -1279,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: [
@@ -1641,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"