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

Useless import

parent 8834c945
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 1 deletion
theories/typing/base.v
+ 0
− 1
View file @ f590d3b5
From lrust.lang Require Export proofmode. From lrust.lang Require Export proofmode.
From lrust.lifetime Require Export frac_borrow.
(* Last, so that we make sure we shadow the defintion of delete for (* Last, so that we make sure we shadow the defintion of delete for
sets coming from the prelude. *) sets coming from the prelude. *)
......
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