aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Case12.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-05-15 16:05:11 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-06-05 22:09:41 -0400
commit9b0376731de3b71a7461747d12763becca1e5399 (patch)
tree4eeaff5d0238034a7232e8b5778419dcd85444aa /test-suite/success/Case12.v
parent13e11b6aec1444071dc3787da15e89a6bc0eb0dc (diff)
Make Ltac Profiling an setting
Diffstat (limited to 'test-suite/success/Case12.v')
0 files changed, 0 insertions, 0 deletions