| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-05-14 | Move the static check of evaluability in unfold tactic to runtime. | Pierre-Marie Pédrot | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |