aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2014-12-27Revert "Term: include a function to print terms"Enrico Tassi
2014-12-26Term: include a function to print termsEnrico Tassi
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-18Fixed bad newlines in output for std output and emacs.Pierre Courtieu
2014-12-16msg_info now puts infomsg tag in emacs mode.Pierre Courtieu
2014-12-15Changed bullet informations to warning for better display in PG.Pierre Courtieu
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-12-12Searchxxx now search also the hypothesis and support goal selector.Pierre Courtieu
2014-12-04Improving error message when one instance-hole is not found.Hugo Herbelin
2014-11-30Fixing printing of dirpathes in Ppconstr. It was reversed.Pierre-Marie Pédrot
2014-11-25Adding tag output to references in Ppconstr.Pierre-Marie Pédrot
2014-11-24Plugging console highlighting in for toplevel and compilation error messages.Pierre-Marie Pédrot
2014-11-22Removing useless flag of the historical move tactic.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 14:46:37 +0000