diff options
| author | herbelin | 2009-12-12 19:09:28 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-12 19:09:28 +0000 |
| commit | c94207ce53c82652e2b5841da55cd5de5266445d (patch) | |
| tree | 8b0a93f8481c54e8e480981ac9f42fce30d26ec7 /plugins/ring/ring.ml | |
| parent | 5594ef1bdffce56816d09bce175b722f1a795bed (diff) | |
Improved the rendering of "dependent rewrite" and hence of "inversion"
by contracting in advance the projT (existT ...) redexes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12577 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/ring/ring.ml')
0 files changed, 0 insertions, 0 deletions