diff options
author | Vincent Laporte <vbgl@users.noreply.github.com> | 2019-11-12 14:56:04 +0000 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-11-12 15:56:04 +0100 |
commit | 5b23665719a332db987f8f8b7c0e64667d0d521e (patch) | |
tree | 7e0f27fbd3a38a9b360f5fb59f73686a87c4a228 /cparser/Checks.mli | |
parent | 029329c8adc955d9ebe9030074cce0df9dcfa5f7 (diff) | |
download | compcert-5b23665719a332db987f8f8b7c0e64667d0d521e.tar.gz compcert-5b23665719a332db987f8f8b7c0e64667d0d521e.zip |
Use `intuition idtac` instead of `intuition` (#321)
A stronger `intuition` in the near future would break this use of `intuition`.
Diffstat (limited to 'cparser/Checks.mli')
0 files changed, 0 insertions, 0 deletions