aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_using.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-22 21:09:05 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-13 12:19:23 +0200
commite3a3b4bb17c40b6af2ef8501c405f0600cc6d65b (patch)
treed038fd28fc8ea222557ce492998a27a723371e04 /proofs/proof_using.ml
parentba88e99d37817cd3a591b14bbceb61e28f3e3382 (diff)
Typo in a comment of plugin Quote.
Diffstat (limited to 'proofs/proof_using.ml')
0 files changed, 0 insertions, 0 deletions