aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-10-13 14:21:22 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-10-18 21:56:56 +0200
commitcb5f55380875bb3029b051eb3acfbb912d83454b (patch)
treed13dfe3e824ee28e95c0325daa2db5002a5bd655 /proofs/goal.ml
parent5ac6c86ad8e18161151d53687da1e2825f0a6b46 (diff)
[pp] Use more convenient pp API in ssrmatching
Diffstat (limited to 'proofs/goal.ml')
0 files changed, 0 insertions, 0 deletions