From 88f3b5a441a3aaeb637d0b109544fbe71b7560dd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Tue, 20 Feb 2018 15:35:25 +0100
Subject: Allow universe declarations for [with Definition].

---
 vernac/comFixpoint.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index edfe7aa81..a794c2db0 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -14,7 +14,6 @@ open Pretyping
 open Evarutil
 open Evarconv
 open Misctypes
-open Vernacexpr
 
 module RelDecl = Context.Rel.Declaration
 
-- 
cgit v1.2.3