aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-11 17:06:13 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-11 17:28:56 +0100
commitac65eef8bbc2e405f1964f35c6a129dfa1755888 (patch)
treed948c59c8fa70d905ca443e7bac8b944f6d8a7a9 /kernel/closure.ml
parente8af74ad7913773c4dfb688167b15b6e15e4397a (diff)
Fixing bug #4019, and checker blow-up at once.
Diffstat (limited to 'kernel/closure.ml')
0 files changed, 0 insertions, 0 deletions