diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-22 01:36:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-22 22:01:50 +0100 |
| commit | 4953a129858a231e64dec636a3bc15a54a0e771c (patch) | |
| tree | 747f4b6deffe19eebef59a4943d1811a375c15a3 /library/lib.mli | |
| 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 'library/lib.mli')
0 files changed, 0 insertions, 0 deletions