diff options
| author |  Jason Gross <jgross@mit.edu> | 2013-11-21 19:36:45 -0500 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2013-12-12 10:06:53 +0100 |
| commit | a9507f72ffb5cb0b594b097c8d1ed137399fca4a (patch) | |
| tree | 9bb8ad8cb861e933b69a808660ba27f0df4fd6d7 /library/libnames.mli | |
| parent | c2bb8e80ad013ae9021937b95ab01f92450341c5 (diff) | |
Generalize eq_proofs_unicity
The generalizded version is eq_proofs_unicity_one_var. We preserve
backwards compatibility, unless someone used nu_left_inv (which was
defined as a Remark(!), but whose type depended on a number of Lets.)
We could keep going in defining one variable variants, but I was lazy.
I'm also not sure if we should be breaking backward compatiblity to
generalize these theorems, if we should make separate files for the
pointed versions, or if we should just have duplicate theorems in each
file. (I'm also not sure if I should call it _one_var or _pointed or
something else.)
This closes Bug 3019.
Diffstat (limited to 'library/libnames.mli')
0 files changed, 0 insertions, 0 deletions