diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-11 17:06:13 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-11 17:28:56 +0100 |
commit | ac65eef8bbc2e405f1964f35c6a129dfa1755888 (patch) | |
tree | d948c59c8fa70d905ca443e7bac8b944f6d8a7a9 /checker/term.ml | |
parent | e8af74ad7913773c4dfb688167b15b6e15e4397a (diff) |
Fixing bug #4019, and checker blow-up at once.
Diffstat (limited to 'checker/term.ml')
0 files changed, 0 insertions, 0 deletions