diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-28 18:29:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-29 15:36:54 +0200 |
| commit | adbc03f4ec1fa8d21343fc252b1462b582665aeb (patch) | |
| tree | 0898035aae5310250331cff8a985f1849eaeda49 /pretyping/tacred.ml | |
| parent | a6ea8b53198fbe6cc1740f8cc84c02b277b1d2ac (diff) | |
Move Params definition in generalize rewriting out of a section so that
its universe doesn't get constrained unnecessarily (bug found in MathClasse).
Also avoid using rewrite itself in a proof in Morphisms.
Diffstat (limited to 'pretyping/tacred.ml')
0 files changed, 0 insertions, 0 deletions