diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v index 7aa0023f..47e04bec 100644 --- a/theories/proofmode/tokens.v +++ b/theories/proofmode/tokens.v @@ -1,4 +1,3 @@ -Require Import Coq.Strings.Ascii. From iris.proofmode Require Import base. Set Default Proof Using "Type".