printing · coq · Tangled

forked from coq/coq

coq printing

13 files

Pierre Roux · Turn notation into a record · 3w ago

Remove compat coq-core libraries (not executables)

Stop going through genargs to print values in Pptactic.pr_value

Stop going through genargs to print values in Pptactic.pr_value

Turn notation into a record

Implement `{| foo with fields |}` for terms

Abstract away the Summary reference type.

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

Cleanup beautify handling

Avoid printing extra parens in Pputil.pr_*_generic

Tiny cleanup in assumptions printing code

feat: per-definition ImpredicativeSet in Print Assumptions

reversiblePrinting.ml

Add Printing Reversible flags: check printed terms reparse to equal terms, escalating printing options when not

reversiblePrinting.mli

Add Printing Reversible flags: check printed terms reparse to equal terms, escalating printing options when not