diff options
| author | Paolo G. Giarrusso | 2020-05-03 01:50:40 +0200 |
|---|---|---|
| committer | Paolo G. Giarrusso | 2020-05-03 01:50:40 +0200 |
| commit | c52756a8fda857b0b7051a73d3afbb90aa5be5e9 (patch) | |
| tree | c75c8cf07dfebba6d855a33970e57339d410f757 /test-suite/output/ErrorInModule.v | |
| parent | f129326d545ae27d362132b279167d119894a992 (diff) | |
Ensure eintros allows creating evars
Thread the `ev` (an `evar_flag`) appropriately through `intros0`.
Discussed on https://gitter.im/coq/coq?at=5eacace7f0377f16316083b8.
Diffstat (limited to 'test-suite/output/ErrorInModule.v')
0 files changed, 0 insertions, 0 deletions