aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2014-11-20Setting printing flags on the printing of mutual inductives.Pierre-Marie Pédrot
2014-11-20Moving mutual inductive printing from Printer to Printmod.Pierre-Marie Pédrot
2014-11-19Print [uconstr] in genargs.Arnaud Spiwack
2014-11-19Proper printer for [uconstr] in [Pptactic].Arnaud Spiwack
2014-11-19Printing function for [uconstr].Arnaud Spiwack
2014-11-19Adding rich-printing facilities to Printmod.Pierre-Marie Pédrot
2014-11-17Adding notation terminals to coqtop highlight.Pierre-Marie Pédrot
2014-11-17Fixing semantics of Ppconstr.print_hunks.Pierre-Marie Pédrot
2014-11-17Missing keywords in Ppconstr.Pierre-Marie Pédrot
2014-11-17Setting printing tags for Ltac.Pierre-Marie Pédrot
2014-11-17Moving printing code for red_expr and may_eval to Pptactic.Pierre-Marie Pédrot
2014-11-17Default styles for printing tags.Pierre-Marie Pédrot
2014-11-17Setting error tag on generic errors returned by Coqtop.Pierre-Marie Pédrot
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-15Adding tags to messages.Pierre-Marie Pédrot
2014-11-15Additional style tags for constrs.Pierre-Marie Pédrot
2014-11-15Setting a keyword tag in Ppconstr.Pierre-Marie Pédrot
2014-11-15Adding a pretty-printing style library.Pierre-Marie Pédrot
2014-11-13Move conjugate_verb_to_be next to cString.plural.Hugo Herbelin
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-05lib/RichPp: Rename into Richpp.Yann Régis-Gianas
2014-11-05printing/Ppvernac: Fix missing keyword tagging on theorem introducers.Yann Régis-Gianas
2014-11-05printing/Ppvernac: Fix missing keyword tagging on definition introducers.Yann Régis-Gianas
2014-11-05printing/Ppvernac: Cosmetics.Yann Régis-Gianas
2014-11-04printing/Ppannotation: New annotation for tactic syntactic objects.Regis-Gianas
2014-11-04printing/Pptactic.Make: New.Regis-Gianas
2014-11-04printing/Pptacticsig: New signature for tactic pretty-printers.Regis-Gianas
2014-11-04lib/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04Rebase artefact.Regis-Gianas
2014-11-04lib/Pp.tag: New.Regis-Gianas
2014-11-04printing/Ppannotation: Introduce a new annotation for keywords.Regis-Gianas
2014-11-04printing/richPrinter: Fix incorrect signatures.Regis-Gianas
2014-11-04printing/RichPrinter: New API for rich pretty-printing.Regis-Gianas
2014-11-04Ppvernac: Publish new rich pretty-printer.Regis-Gianas
2014-11-04Ppannotation.t: New constructor AVernac.Regis-Gianas
2014-11-04Ppvernacsig: New.Regis-Gianas
2014-11-04Ppvernac.Make: NewRegis-Gianas
2014-11-04Ppvernac: Cosmetics.Regis-Gianas
2014-11-04Ppannotation: New.Regis-Gianas
2014-11-04printing/Ppconstr.Make:Regis-Gianas
2014-11-04printing/Ppconstr.print_hunks:Regis-Gianas
2014-11-04printing/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04Removing the old rename tactic.Pierre-Marie Pédrot
2014-11-01Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Arnaud Spiwack
2014-11-01Info: print a name for the primitive tactics in [Proofview].Arnaud Spiwack
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-22Pushing Pierre's factorization of names in goal context printing fromHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 13:51:26 +0000