Replace one `intuition` by `intuition auto`HEADmaster

1 files changed, 1 insertions, 1 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 3fdbacb..f0be801 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1976,7 +1976,7 @@ Remark addressing_not_long:
 Proof.
   intros. inv H.
   assert (A: forall ty, In ty (type_of_addressing addr) -> ty = Tptr).
-  { intros. destruct addr; simpl in H; intuition. }
+  { intros. try (apply diff_false_true in H0). destruct addr; simpl in H; intuition auto. }
   assert (B: In (env r) (type_of_addressing addr)).
   { rewrite <- H5. apply in_map; auto. }
   assert (C: env r = Tint).