aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
...
* 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
* printing/Pptactic.Make: New.Gravatar Regis-Gianas2014-11-04
* printing/Pptacticsig: New signature for tactic pretty-printers.Gravatar Regis-Gianas2014-11-04
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
* Rebase artefact.Gravatar Regis-Gianas2014-11-04
* lib/Pp.tag: New.Gravatar Regis-Gianas2014-11-04
* printing/Ppannotation: Introduce a new annotation for keywords.Gravatar Regis-Gianas2014-11-04
* printing/richPrinter: Fix incorrect signatures.Gravatar Regis-Gianas2014-11-04
* printing/RichPrinter: New API for rich pretty-printing.Gravatar Regis-Gianas2014-11-04
* Ppvernac: Publish new rich pretty-printer.Gravatar Regis-Gianas2014-11-04
* Ppannotation.t: New constructor AVernac.Gravatar Regis-Gianas2014-11-04
* Ppvernacsig: New.Gravatar Regis-Gianas2014-11-04
* Ppvernac.Make: NewGravatar Regis-Gianas2014-11-04
* Ppvernac: Cosmetics.Gravatar Regis-Gianas2014-11-04
* Ppannotation: New.Gravatar Regis-Gianas2014-11-04
* printing/Ppconstr.Make:Gravatar Regis-Gianas2014-11-04
* printing/Ppconstr.print_hunks:Gravatar Regis-Gianas2014-11-04
* printing/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
* Removing the old rename tactic.Gravatar Pierre-Marie Pédrot2014-11-04
* Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Gravatar Arnaud Spiwack2014-11-01
* Info: print a name for the primitive tactics in [Proofview].Gravatar Arnaud Spiwack2014-11-01
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Emit a warning for void Arguments statement (Close 3713)Gravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Removing Convert_concl and Convert_hyp from Logic.Gravatar Hugo Herbelin2014-10-09
* Going back on granting wish #1039 in f5d7b2b1e so that apply withGravatar Hugo Herbelin2014-10-01
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Printing evar instance in a more intuitive order.Gravatar Hugo Herbelin2014-09-29
* Fix printing of primitive record info.Gravatar Matthieu Sozeau2014-09-29
* Print information about primitive records (Print and About).Gravatar Matthieu Sozeau2014-09-28
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-09-25
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
* Fix a message.Gravatar Arnaud Spiwack2014-09-24
* coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Gravatar Arnaud Spiwack2014-09-24
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 08:49:13 +0000