diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-24 16:29:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-27 18:49:46 +0200 |
| commit | 46a7ac14e5803d1690584ac939889ecc03ab0dd4 (patch) | |
| tree | 56c25d70d7db893debd5e49a31bf3c2d064f8fae /plugins/cc/cctac.ml | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Congruence: getting rid of a detour by the compatibility layer of proof engine.
The V82 compatibility layer of the proof engine was used by cc
(congruence closure) for the sole purpose of maintaining an
environment and a sigma. We inline the corresponding env and sigma in
the state of cc algorithm to get rid of the compatibility layer.
Diffstat (limited to 'plugins/cc/cctac.ml')
0 files changed, 0 insertions, 0 deletions