aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorArnaud Spiwack2014-07-23 15:14:24 +0200
committerArnaud Spiwack2014-07-23 17:43:18 +0200
commit474197250baa3366385563bc5403a0871d106275 (patch)
treee66c039faa15124113a0c832a7f08d70af155ac7 /kernel/type_errors.ml
parentab4d3bae45265d18357bacbdeeefb7018f1e58c5 (diff)
Proof_global: an unused variable replaced by a wildcard.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions