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 /lib/IntvSets.v | |
| parent | 029329c8adc955d9ebe9030074cce0df9dcfa5f7 (diff) | |
| download | compcert-kvx-5b23665719a332db987f8f8b7c0e64667d0d521e.tar.gz compcert-kvx-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 'lib/IntvSets.v')
| -rw-r--r-- | lib/IntvSets.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/IntvSets.v b/lib/IntvSets.v index 78c20cc5..b97d9882 100644 --- a/lib/IntvSets.v +++ b/lib/IntvSets.v @@ -102,7 +102,7 @@ Proof. simpl. rewrite IHok. tauto. destruct (zlt h0 l). simpl. tauto. - rewrite IHok. intuition. + rewrite IHok. intuition idtac. assert (l0 <= x < h0 \/ l <= x < h) by xomega. tauto. left; xomega. left; xomega. |