coqpp · coq · Tangled

Sign in Join now

coq stepbrobd.com /

Star Starred Star 1

Something went wrong. Try again.

Watch Watching Watch

forked from coq/coq

Star Starred Star 1

Something went wrong. Try again.

Watch Watching Watch

Overview Overview Issues Issues Pulls Pulls Pipelines Pipelines

coq /coqpp

10 files

Gaëtan Gilbert · PIDENT with exact ident and PKEYWORD have type `unit p` · 2mo ago

Make it possible to warn when interning a TACTIC EXTEND + use for ssr rewrite

Update the OCaml headers to reflect the fact Coq is now Rocq.

Make it possible to warn when interning a TACTIC EXTEND + use for ssr rewrite

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

Turn coqpp_main into a library file

coqpp_parse.mly

Make it possible to warn when interning a TACTIC EXTEND + use for ssr rewrite

coqpp_parser.ml

Update the OCaml headers to reflect the fact Coq is now Rocq.

coqpp_parser.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Turn coqpp_main into a library file

Use `rocq pp-mlg` for rocq-runtime files, move `coqpp` back to `coq-core`