diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-27 22:08:57 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-27 22:08:57 +0000 |
| commit | 42ea537affb88f8e63499d909eb526e024fc0aec (patch) | |
| tree | 15d95ea521cd5b5ee592cee7c818cf45b413debf /tactics/equality.mli | |
| parent | fdad03c5c247ab6cfdde8fd58658d9e40a3fd8aa (diff) | |
Fix "Existing Instance" to handle globality information and "Existing
Class" too to handle references instead of just idents. Minor fix in
coqdoc. zeta-normalize setoid_rewrite proofs, removing useless
let-bindings generated by the tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
0 files changed, 0 insertions, 0 deletions