aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ltac.out
Commit message (Expand)AuthorAge
* Printing again "intros **" as "intros" by default.Gravatar Hugo Herbelin2017-11-24
* Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-24
* Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
* Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
|\
* | Adding a test for #4398 (interpretation scopes for "match goal").Gravatar Hugo Herbelin2016-10-24
* | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-22
|\ \
| * | Fixing printing of generic arguments of tag "var".Gravatar Hugo Herbelin2016-10-22
| | * [pp] Try to properly tag error messages in cError.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |/ |/|
* | Fix output test-suite after commit 0d3c319.Gravatar Pierre-Marie Pédrot2016-09-09
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* | About printing of traces of failures while calling ltac code.Gravatar Hugo Herbelin2016-06-06
* | A small test of Print Ltac.Gravatar Hugo Herbelin2016-04-09
|/
* Refining 0c320e79ba30 in fixing interpretation of constr under bindersGravatar Hugo Herbelin2015-10-11