From df038c9332a72fdf620d9682e931ec5789f242c4 Mon Sep 17 00:00:00 2001
From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
Date: Sat, 27 Apr 2024 17:46:04 +0200
Subject: [PATCH] Add Fixpoint and CoFixpoint in Search logical_kind

This makes it possible e.g. to
```
Search (nat -> nat -> nat) [is:Fixpoint | is:Definition].
```
---
 vernac/g_vernac.mlg | 2 ++
 1 file changed, 2 insertions(+)

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 }