diff options
| author | Maxime Dénès | 2019-04-04 22:08:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:43 +0200 |
| commit | dd672f839765c656a910ff8e07603858dbc8bc38 (patch) | |
| tree | 5266f2fe3b129cfe887e7174c4ec5901e5e3f8b1 /interp/implicit_quantifiers.ml | |
| parent | bf5f0520cf105afb048c6eac5d6de1d3e1a719df (diff) | |
Move vernac-related part of coercions to vernac
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions