aboutsummaryrefslogtreecommitdiffstats
path: root/src/zchaff/zchaff.ml
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2016-04-26 00:30:35 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2016-04-26 00:30:35 +0200
commit9f9699c8134ed0ded42aad64e00cfb9f0a60c914 (patch)
tree2e34b34bf43380bfbdcf6e57fd41cc5773b0b3c6 /src/zchaff/zchaff.ml
parent5ebe1f1c3684609dc0c2f360cf4d86486795ab54 (diff)
downloadsmtcoq-9f9699c8134ed0ded42aad64e00cfb9f0a60c914.tar.gz
smtcoq-9f9699c8134ed0ded42aad64e00cfb9f0a60c914.zip
- Solved the Coq 8.5 problem relating to declaring section variables
- Correct equality check of atoms and formulas for processing congruence closure
Diffstat (limited to 'src/zchaff/zchaff.ml')
0 files changed, 0 insertions, 0 deletions