Update doc/tools/docgram/common.edit_mlg

Co-authored-by: Jim Fehrle <[email protected]>
Villetaneuse · May 16, 2024 · ce5f644 · ce5f644
1 parent 8dbbcd6
commit ce5f644
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
@@ -1971,12 +1971,12 @@ logical_kind: [
 | DELETE "Instance"
 | DELETE "Scheme"
 | DELETE "Canonical"
+| [  "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" ]
 | DELETE "Fixpoint"
 | DELETE "CoFixpoint"
-| [  "Coercion" | "Instance" | "Scheme" | "Canonical" | "SubClass" | "Fixpoint" | "CoFixpoint" ]
 | DELETE "Field"
 | DELETE "Method"
-| [ "Field" | "Method" ]
+| [  "Fixpoint" | "CoFixpoint" | "Field" | "Method" ]
 ]
 
 (* ltac2 *)