aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
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
2014-10-01Going back on granting wish #1039 in f5d7b2b1e so that apply withHugo Herbelin
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-09-29Printing evar instance in a more intuitive order.Hugo Herbelin
2014-09-29Fix printing of primitive record info.Matthieu Sozeau
2014-09-28Print information about primitive records (Print and About).Matthieu Sozeau
2014-09-25Improve consistency of whitespace (beautifier).Xavier Clerc
2014-09-24Using an or_var rather than the hack with loc for coding a pure identHugo Herbelin
2014-09-24Fix a message.Arnaud Spiwack
2014-09-24coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".Arnaud Spiwack
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-15Not printing goal name (reinstalled by mistake in a previous commit).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 17:21:15 +0000