From 5b23665719a332db987f8f8b7c0e64667d0d521e Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 12 Nov 2019 14:56:04 +0000 Subject: Use `intuition idtac` instead of `intuition` (#321) A stronger `intuition` in the near future would break this use of `intuition`. --- lib/IntvSets.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/IntvSets.v') 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. -- cgit