diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-09 18:23:23 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-09 18:23:23 +0000 |
| commit | 43fede22d500a7234a82aaae77adfebff8006c4f (patch) | |
| tree | bedcaff6b1ad79330f39f33b38cce4c0208bb733 /tactics/autorewrite.ml | |
| parent | 2cf5036431304d5a3e6393d5fd5827798ea98983 (diff) | |
Fix bug #2317: setoid_rewrite ignored binding lists. Slightly
generalize the interface of Clenv to be able to use the existing
treatment of bindings. Clenv functions did not use goals conclusions
but insisted on getting goals anyway (which is even more problematic as
goals appear in evar maps now).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13102 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/autorewrite.ml')
0 files changed, 0 insertions, 0 deletions