diff options
| author | Frédéric Besson | 2014-08-01 15:23:24 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2014-08-01 15:23:24 +0200 |
| commit | bbf3682aa80bb86502e29018465e3602f0d9bb3e (patch) | |
| tree | 030cea0b019df4903664fe77d96297c40381762a /kernel/type_errors.ml | |
| parent | 7e67bba64e1b59be2acf5997157bff10581d28f2 (diff) | |
micromega : improve efficiency/termination of type-checking
* unused terms are generalised
* proof is abstract
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions