From 141fb84fb5e69047489710d56636feb30af42743 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 24 Aug 2018 17:14:39 +0200
Subject: [PATCH] Export Ascii for compat with new Coq

---
 theories/proofmode/base.v   | 2 +-
 theories/proofmode/tokens.v | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 2fe6e8f72..a4b54719b 100644
--- 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
index 47e04bec3..7aa0023f2 100644
--- 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".
 
-- 
GitLab