From c9d7e13cbe125a708ce4d4afd9473bae80cc09fc Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 22 Mar 2020 20:34:43 +0000
Subject: Add compcert library to coquplib

---
 src/common/Coquplib.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/common/Coquplib.v')

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index b801756..310efa5 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -23,6 +23,10 @@ From Coq Require Export
      List
      Bool.
 
+(* Depend on CompCert for the basic library, as they declare and prove some
+   useful theorems. *)
+From compcert.lib Require Export Coqlib.
+
 Ltac unfold_rec c := unfold c; fold c.
 
 Ltac solve_by_inverts n :=
-- 
cgit