Skip to content

Commit

Permalink
Add Fixpoint and CoFixpoint in Search logical_kind
Browse files Browse the repository at this point in the history
This makes it possible e.g. to
```
Search (nat -> nat -> nat) [is:Fixpoint | is:Definition].
```
  • Loading branch information
Villetaneuse committed Apr 27, 2024
1 parent 5e0a71c commit df038c9
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions vernac/g_vernac.mlg
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down

0 comments on commit df038c9

Please sign in to comment.