aboutsummaryrefslogtreecommitdiff
path: root/test-suite/ltac2
ModeNameSize
-rw-r--r--compat.v1109logplain
-rw-r--r--errors.v269logplain
-rw-r--r--example1.v572logplain
-rw-r--r--example2.v4001logplain
-rw-r--r--matching.v1723logplain
-rw-r--r--quot.v656logplain
-rw-r--r--rebind.v479logplain
d---------stuff35logplain
-rw-r--r--tacticals.v516logplain
-rw-r--r--typing.v1205logplain