From 55b925c9feef59b17692aaa6f8c8113500e2f2d2 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Wed, 12 May 2021 11:20:18 +0200 Subject: [PATCH] Cleanup imports --- theories/typing/product_split.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v index 8e3e8ec2..3dc9c1ce 100644 --- a/theories/typing/product_split.v +++ b/theories/typing/product_split.v @@ -1,7 +1,8 @@ From iris.algebra Require Import numbers. From iris.proofmode Require Import tactics. From lrust.typing Require Export type. -From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor. +From lrust.typing Require Import type_context lft_contexts product own uniq_bor. +From lrust.typing Require Import shr_bor. Set Default Proof Using "Type". Section product_split. -- GitLab