parsing · coq · Tangled

forked from coq/coq

coq parsing

18 files

coqbot-app[bot] · Merge PR #22601: Reduce the combinatorics of the grammar state access in Grammar API. · 3w ago

PIDENT with exact ident and PKEYWORD have type `unit p`

PIDENT with exact ident and PKEYWORD have type `unit p`

Remove compat coq-core libraries (not executables)

A richer type system for notation variables.

A richer type system for notation variables.

Turn notation into a record

Remove deprecated syntax `foo@{q|u}` (including `Type` version)

Gramlib: more level recovery warnings

Rename the Pcoq module into Procq.

notation_gram.mli

Inline binder_constr

A richer type system for notation variables.

notgram_ops.mli

A richer type system for notation variables.

Introduce a deprecated module alias for Pcoq.

Introduce a deprecated module alias for Pcoq.

Reduce the combinatorics of the grammar state access in Grammar API.

Reduce the combinatorics of the grammar state access in Grammar API.

Match number tokens using NumTok.Unsigned.equal directly.

PIDENT with exact ident and PKEYWORD have type `unit p`