Use intuition idtac instead of intuition (#321)

vbgl · xavierleroy · commit 5b23665719a3 · 2019-11-12T15:56:04.000+01:00
A stronger `intuition` in the near future would break this use of `intuition`.
diff --git 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.
