aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ltac.v
AgeCommit message (Expand)Author
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-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-11Fixing test-suiteHugo Herbelin
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin