aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-27 11:31:02 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-28 12:31:11 +0200
commitd01e3b07470ab326f5754332ac812f21794721bc (patch)
tree0a6c2db31cd1987f6ef18633974c6c20148b00dd /vernac/obligations.ml
parentebfed8fc20c6cad1eddd5057d191905b42630b4e (diff)
A fix for #5598 (no discharge of Existing Classes referring to local variables).
Diffstat (limited to 'vernac/obligations.ml')
0 files changed, 0 insertions, 0 deletions