From 9f5586d88880cbb98c92edfe9c33c76564f1a19c Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Fri, 16 Jan 2015 22:17:03 +0100
Subject: Make native compiler handle universe polymorphic definitions.

One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
---
 kernel/subtyping.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index fa4f1c7c9..db155e6c8 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -17,6 +17,7 @@ open Names
 open Univ
 open Term
 open Declarations
+open Declareops
 open Reduction
 open Inductive
 open Modops
-- 
cgit v1.2.3