Skip to content
Snippets Groups Projects
Commit f30f9831 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Fix Require.

parent c1dba573
No related branches found
No related tags found
No related merge requests found
Pipeline #19770 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/typing/base.v
+ 1
− 1
View file @ f30f9831
...@@ -3,7 +3,7 @@ From gpfsl.base_logic Require Import na. ...@@ -3,7 +3,7 @@ From gpfsl.base_logic Require Import na.
(* Last, so that we make sure we shadow the definition of delete for (* Last, so that we make sure we shadow the definition of delete for
sets coming from the prelude. *) sets coming from the prelude. *)
From lrust.lang.lib Require Export new_delete. From lrust.lang Require Export new_delete.
Open Scope Z_scope. Open Scope Z_scope.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment