3 files changed, 9 insertions, 14 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index b932fc6e30..48d399dfd3 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -365,7 +365,6 @@ term100: [
 | REPLACE term99 ":" term200
 | WITH term99 ":" type
 | MOVETO term_cast term99 ":" type
-| MOVETO term_cast term99 ":>"
 ]
 
 constr: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 47c758b5e8..b5a234a86a 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1,6 +1,15 @@
 (* Coq grammar generated from .mlg files.  Do not edit by hand.  Not compiled into Coq *)
 DOC_GRAMMAR
 
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" natural "."
+| test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
+| Pvernac.Vernac_.main_entry
+]
+
 Constr.ident: [
 | Prim.ident
 ]
@@ -75,7 +84,6 @@ term100: [
 | term99 "<:" term200
 | term99 "<<:" term200
 | term99 ":" term200
-| term99 ":>"
 | term99
 ]
 
@@ -478,15 +486,6 @@ strategy_level: [
 | "transparent"
 ]
 
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "BackTo" natural "."
-| test_show_goal "Show" "Goal" natural "at" natural "."
-| "Show" "Proof" "Diffs" OPT "removed" "."
-| Pvernac.Vernac_.main_entry
-]
-
 opt_hintbases: [
 |
 | ":" LIST1 IDENT
@@ -1774,7 +1773,6 @@ simple_tactic: [
 | "zify_iter_let" tactic      (* micromega plugin *)
 | "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 *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index b0a7cb91f9..cd96693bf0 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -553,7 +553,6 @@ term_cast: [
 | term10 ":" type
 | term10 "<:" type
 | term10 "<<:" type
-| term10 ":>"
 ]
 
 term_match: [
@@ -1856,7 +1855,6 @@ simple_tactic: [
 | "zify_iter_let" ltac_expr      (* micromega plugin *)
 | "zify_elim_let"      (* micromega plugin *)
 | "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      (* ring plugin *)
 | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)