Export Ascii for compat with new Coq

izgzhen · Aug 24, 2018 · 141fb84 · 141fb84
1 parent f891015
commit 141fb84
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
@@ -1,6 +1,6 @@
 From stdpp Require Export strings.
 From iris.algebra Require Export base.
-From Coq Require Import Ascii.
+From Coq Require Export Ascii.
 Set Default Proof Using "Type".
 
 (** * Utility definitions used by the proofmode *)

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