aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Continuing 785f82ee1 on reverting not only f5d7b2b1e but alsoGravatar Hugo Herbelin2015-01-08
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Revert "Term: include a function to print terms"Gravatar Enrico Tassi2014-12-27
* Term: include a function to print termsGravatar Enrico Tassi2014-12-26
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
* Changed bullet informations to warning for better display in PG.Gravatar Pierre Courtieu2014-12-15
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Improving error message when one instance-hole is not found.Gravatar Hugo Herbelin2014-12-04
* Fixing printing of dirpathes in Ppconstr. It was reversed.Gravatar Pierre-Marie Pédrot2014-11-30
* Adding tag output to references in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-25
* Plugging console highlighting in for toplevel and compilation error messages.Gravatar Pierre-Marie Pédrot2014-11-24
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
* Setting printing flags on the printing of mutual inductives.Gravatar Pierre-Marie Pédrot2014-11-20
* Moving mutual inductive printing from Printer to Printmod.Gravatar Pierre-Marie Pédrot2014-11-20
* Print [uconstr] in genargs.Gravatar Arnaud Spiwack2014-11-19
* Proper printer for [uconstr] in [Pptactic].Gravatar Arnaud Spiwack2014-11-19
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* Adding rich-printing facilities to Printmod.Gravatar Pierre-Marie Pédrot2014-11-19
* Adding notation terminals to coqtop highlight.Gravatar Pierre-Marie Pédrot2014-11-17
* Fixing semantics of Ppconstr.print_hunks.Gravatar Pierre-Marie Pédrot2014-11-17
* Missing keywords in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-17
* Setting printing tags for Ltac.Gravatar Pierre-Marie Pédrot2014-11-17
* Moving printing code for red_expr and may_eval to Pptactic.Gravatar Pierre-Marie Pédrot2014-11-17
* Default styles for printing tags.Gravatar Pierre-Marie Pédrot2014-11-17
* Setting error tag on generic errors returned by Coqtop.Gravatar Pierre-Marie Pédrot2014-11-17
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Adding tags to messages.Gravatar Pierre-Marie Pédrot2014-11-15
* Additional style tags for constrs.Gravatar Pierre-Marie Pédrot2014-11-15
* Setting a keyword tag in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-15
* Adding a pretty-printing style library.Gravatar Pierre-Marie Pédrot2014-11-15
* Move conjugate_verb_to_be next to cString.plural.Gravatar Hugo Herbelin2014-11-13
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* lib/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppvernac: Fix missing keyword tagging on theorem introducers.Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppvernac: Fix missing keyword tagging on definition introducers.Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppvernac: Cosmetics.Gravatar Yann Régis-Gianas2014-11-05
* printing/Ppannotation: New annotation for tactic syntactic objects.Gravatar Regis-Gianas2014-11-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 23:30:52 +0000