aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorFrédéric Besson2014-08-01 15:23:24 +0200
committerFrédéric Besson2014-08-01 15:23:24 +0200
commitbbf3682aa80bb86502e29018465e3602f0d9bb3e (patch)
tree030cea0b019df4903664fe77d96297c40381762a /kernel
parent7e67bba64e1b59be2acf5997157bff10581d28f2 (diff)
micromega : improve efficiency/termination of type-checking
* unused terms are generalised * proof is abstract
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions