diff options
| author | Matthieu Sozeau | 2014-06-13 14:38:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-13 17:40:27 +0200 |
| commit | f49137b917fa7561eb53a87155ed57b3dbc70d90 (patch) | |
| tree | 4d209f1fa70c0204074c691e3b2be579a7d8e999 /plugins/xml/xmlcommand.ml | |
| parent | 1681238424c2d46e7a31467212d4daed4b30a827 (diff) | |
HoTT/coq bug #7 is closed, and the definitions can be made to go through using explicit
universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
0 files changed, 0 insertions, 0 deletions