aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ltac.out
AgeCommit message (Expand)Author
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2018-09-10Fixing an inconsistency in interpreting Ltac names linking to binder names.Hugo Herbelin
2017-11-24Printing again "intros **" as "intros" by default.Hugo Herbelin
2017-11-24Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
2017-11-20Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
2017-03-21[pp] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
2016-10-24Adding a test for #4398 (interpretation scopes for "match goal").Hugo Herbelin
2016-10-22Merge branch 'v8.5' into v8.6Hugo Herbelin
2016-10-22Fixing printing of generic arguments of tag "var".Hugo Herbelin
2016-10-18[pp] Try to properly tag error messages in cError.Emilio Jesus Gallego Arias
2016-09-09Fix output test-suite after commit 0d3c319.Pierre-Marie Pédrot
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-06About printing of traces of failures while calling ltac code.Hugo Herbelin
2016-04-09A small test of Print Ltac.Hugo Herbelin
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:14:59 +0000