From f30f9831ec6eda189003e0a010f1c0a3831bc6f4 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 15 Sep 2019 22:18:09 +0200
Subject: [PATCH] Fix Require.
---
theories/typing/base.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/base.v b/theories/typing/base.v
index 796d2243..cd2a0b9b 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -3,7 +3,7 @@ From gpfsl.base_logic Require Import na.
(* Last, so that we make sure we shadow the definition of delete for
sets coming from the prelude. *)
-From lrust.lang.lib Require Export new_delete.
+From lrust.lang Require Export new_delete.
Open Scope Z_scope.
--
GitLab