aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-09-28 15:38:33 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-10-22 11:57:58 +0200
commit80d5779409bf33fbe5043275b96775a5f04a3b2c (patch)
tree7e38bd03ccf57a9c24971441bfa57d0a792edfbe /theories/Bool
parentcc2778c3310a75585c00f0eb659ddde7aee2944a (diff)
Remove incorrect assertion in cbn (bug #4822).
This assertion checked that two arguments in the same position were equal, but in fact, since one might have already been reduced, they are only convertible (which is too costly to check in an assertion).
Diffstat (limited to 'theories/Bool')
0 files changed, 0 insertions, 0 deletions