diff options
| author | Pierre-Marie Pédrot | 2020-05-05 14:19:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-14 12:38:08 +0200 |
| commit | be56f39ecfc0726772cc6930dbc7657348f008e1 (patch) | |
| tree | f8405fd9fbfb209a037d979b60efeb44dd928438 /interp/notation.mli | |
| parent | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff) | |
Move the static check of evaluability in unfold tactic to runtime.
See #11840 for a motivation. I had to fix Floats.FloatLemmas because
it uses the same name for a notation and a term, and the fact this
unfold was working on this was clearly a bug. I hope nobody relies
on this kind of stuff in the wild.
Fixes #5764: "Cannot coerce ..." should be a runtime error.
Fixes #5159: "Cannot coerce ..." should not be an error.
Fixes #4925: unfold gives error on Admitted.
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions