aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-09-03 10:32:50 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-09-03 20:41:34 +0200
commit2c96be02dfa0a6169856a844dfc36b7f1053d0c5 (patch)
tree236c961788453eb3fd0385c04e91abcaa71e1a17 /proofs/goal.ml
parent6119a0e4f760ff944351570e90487f066db42858 (diff)
Yes another remaining clearing bug with 'apply in'.
Diffstat (limited to 'proofs/goal.ml')
0 files changed, 0 insertions, 0 deletions