From 0acafd481fc25790723b6388aa750c6a549d4881 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Oct 2018 08:23:13 +0200
Subject: [PATCH] Remove spurious import.

---
 tests/proofmode.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 0cc6d3cb0..b71cbbf74 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics intro_patterns.
-From stdpp Require Import gmap hlist.
 Set Default Proof Using "Type".
 
 Section tests.
-- 
GitLab