From f6f537dd60336b599c9541b0dca56255bdf2ba5e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 27 Aug 2018 11:13:47 -0400
Subject: Import prim token notations before using them

This is required for compatibility with
https://github.com/coq/coq/pull/8064, where prim token notations no longer
follow `Require`, but instead follow `Import`.

Closes #246
Closes #250
---
 lib/Coqlib.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 3fe1ea2e..3b8e5b3b 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -17,6 +17,7 @@
     used throughout the development.  It complements the Coq standard
     library. *)
 
+Require Export String.
 Require Export ZArith.
 Require Export Znumtheory.
 Require Export List.
-- 
cgit