diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-05-31 12:39:38 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 15:59:33 +0000 |
| commit | 767898e6e59e86e3123846374448402360b783e6 (patch) | |
| tree | 9890e3383c32bd46f1f8447eda30e22aa992d23c /vernac/vernacexpr.ml | |
| parent | 8520cc7a02bedf4f4820ef198550f7cfa2a6454c (diff) | |
Allow “Let”-defined coercions
Diffstat (limited to 'vernac/vernacexpr.ml')
0 files changed, 0 insertions, 0 deletions