diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index ada9b14a0217..7b77962270ae 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1248,6 +1248,8 @@ GRAMMAR EXTEND Gram
   extended_def_token:
     [ [ k = def_token -> { snd k }
       | IDENT "Coercion" -> { Coercion }
+      | IDENT "Fixpoint" -> { Fixpoint }
+      | IDENT "CoFixpoint" -> { CoFixpoint }
       | IDENT "Instance" -> { Instance }
       | IDENT "Scheme" -> { Scheme }
       | IDENT "Canonical" -> { CanonicalStructure }