diff options
| author | msozeau | 2009-06-16 18:47:04 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-16 18:47:04 +0000 |
| commit | d1aee3a64abd6399d18e940133069a57a490a45d (patch) | |
| tree | 622464aea7bf6aa6191f00ea762c6943727eb4f9 /pretyping/typeclasses_errors.ml | |
| parent | c5168ac18d40cf347da1a951d23f47777ae477e9 (diff) | |
Reimplementation of leibniz rewrite to control the instantiation of the
rewriting lemma more precisely. This should make rewrite properly fail
when existentials are around instead of giving an identical goal up to
new evars. Also a first step towards adding occurences to the leibniz
rewrite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12192 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions