aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/redexpr.ml
diff options
context:
space:
mode:
authorGravatar xclerc <xavier.clerc@inria.fr>2014-02-24 11:07:21 +0100
committerGravatar xclerc <xavier.clerc@inria.fr>2014-02-24 11:07:21 +0100
commitc4370e5394cc9f678250150bd5bb407629b21913 (patch)
treeaba0aac4e01f5ca2d5e0a6e2a82638fa65dc67bf /proofs/redexpr.ml
parent6b10edbe056f38d784258b6bf3ea4b8dc472e472 (diff)
Fix grammatical mistake in error message (bug #3238)
Diffstat (limited to 'proofs/redexpr.ml')
0 files changed, 0 insertions, 0 deletions