diff options
author | 2014-09-02 11:37:05 +0200 | |
---|---|---|
committer | 2014-09-02 19:28:49 +0200 | |
commit | a50aecc7a56b7b7b1c676009f1936599366eb4ba (patch) | |
tree | 33e55e7e539cf9245fc4dcba8d860cab95e26e0f /tactics/eqdecide.mli | |
parent | 595de46fe3de117129395157dfad28548dc0a157 (diff) |
Another fix than 19a7a5789c to avoid descend_in_conjunction to use
fresh names interferring with names later generated in intropatterns
(as introduced in 72498d6d68ac which passed "clenv_refine_in continued
by pattern introduction" to descend_in_conjunction while only a pure
clenv_refine was passed before). The 72498d6d68ac version was
generating fresh names in the wrong order (morally-private names for
descend_in_conjunction before user-level names in clenv_refine_in).
The 19a7a5789c fix was introducing expressions not handled by the
refine from logic.ml.
In particular, this fixes RelationAlgebra.
Diffstat (limited to 'tactics/eqdecide.mli')
0 files changed, 0 insertions, 0 deletions