aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ltac.out
AgeCommit message (Expand)Author
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