diff options
| author | Théo Zimmermann | 2017-03-14 16:22:24 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-03-14 16:22:24 +0100 |
| commit | 43524c6689f372b32770c20d19866f2f4edb4cc6 (patch) | |
| tree | c7f33910befbc29b79ef13b21352a3b04cf23026 /kernel/cbytecodes.mli | |
| parent | 42f27beb63a629dcef514abb0b31dea193f35a38 (diff) | |
Show unused-intro-pattern warning.
This warning was shown in CoqIDE but not by coqc.
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions