diff options
author | 2016-01-22 01:36:43 +0100 | |
---|---|---|
committer | 2016-01-22 22:01:50 +0100 | |
commit | 4953a129858a231e64dec636a3bc15a54a0e771c (patch) | |
tree | 747f4b6deffe19eebef59a4943d1811a375c15a3 /test-suite/bugs/closed/HoTT_coq_067.v | |
parent | 176d8e004153e65688dc8ef4f22f7939fd6101b1 (diff) |
Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.
It was not detected because of a "bug" in clear checking the existence
of the hypothesis only at interpretation time (not at execution time).
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_067.v')
0 files changed, 0 insertions, 0 deletions