diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2015-12-29 13:21:17 -0500 |
|---|---|---|
| committer |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-04-04 17:08:04 +0200 |
| commit | 4c078b0362542908eb2fe1d63f0d867b339953fd (patch) | |
| tree | 7081179cef1270f35cc5ce8008336761a2a74050 /test-suite/bugs | |
| parent | 59cb5ca9b6c0e29fe65e9ae99dfd6cabafc52be6 (diff) | |
Update Coq84.v
We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
Diffstat (limited to 'test-suite/bugs')
0 files changed, 0 insertions, 0 deletions