aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
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
2014-10-17Experimental printing of the signature of open evars in Check.Hugo Herbelin
2014-10-16Goal: remove most of the API (make [Goal.goal] concrete).Arnaud Spiwack
2014-10-13Emit a warning for void Arguments statement (Close 3713)Enrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-09Removing Convert_concl and Convert_hyp from Logic.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-17 06:18:51 +0000