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 /proofs/goal.mli | |
| 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 'proofs/goal.mli')
| -rw-r--r-- | proofs/goal.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index dc9863156..b8c979ad7 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -64,9 +64,6 @@ module V82 : sig (* Principal part of tclNOTSAMEGOAL *) val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool - (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma - (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map |