diff --git a/tests/proofmode.v b/tests/proofmode.v index 0cc6d3cb030d99e1c51b099a1ef805b3189303dc..b71cbbf74b5972594d4ebfc60ab3b607eab47b40 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -1,5 +1,4 @@ From iris.proofmode Require Import tactics intro_patterns. -From stdpp Require Import gmap hlist. Set Default Proof Using "Type". Section tests.