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 | |
| 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')
| -rw-r--r-- | proofs/goal.ml | 14 | ||||
| -rw-r--r-- | proofs/goal.mli | 3 |
2 files changed, 0 insertions, 17 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index ba7e458f3..6912db364 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -117,20 +117,6 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl extra_hyps = - let evi = Evd.find sigma gl in - let hyps = evi.Evd.evar_hyps in - let new_hyps = - List.fold_right Environ.push_named_context_val extra_hyps hyps in - let filter = evi.Evd.evar_filter in - let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in - let new_evi = - { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in - let new_evi = Typeclasses.mark_unresolvable new_evi in - let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = sigma; } - (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = let evi = Evd.find sigma gl in 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 |