Export Ascii for compat with new Coq

141fb84f · Ralf Jung · f891015e · 141fb84f · 141fb84f
Commit 141fb84f authored Aug 24, 2018 by Ralf Jung
Show whitespace changes
Inline Side-by-side

Showing with 2 additions and 1 deletion

theories/proofmode/base.v theories/proofmode/base.v +1 -1

theories/proofmode/tokens.v theories/proofmode/tokens.v +1 -0

No files found.
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
 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 *)

--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
+Require Import Coq.Strings.Ascii.
 From iris.proofmode Require Import base.
 Set Default Proof Using "Type".