aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorFrédéric Besson2016-09-08 14:19:02 +0200
committerFrédéric Besson2016-09-08 14:19:02 +0200
commit9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf (patch)
tree692212e73e902b4aacf36f23ae5b375016979158 /kernel
parent76a8288c37e68fd8559f903af60abf8c3f87c007 (diff)
Fix Bug #5073 : regression of micromega plugin
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions