From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Sat, 17 Oct 2015 21:40:49 -0700
Subject: Adds support for the virtual machine to perform reduction of universe
 polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
---
 kernel/vars.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/vars.ml')

diff --git a/kernel/vars.ml b/kernel/vars.ml
index 88c1e1038c..a800e25315 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -337,5 +337,5 @@ let subst_instance_context s ctx =
   if Univ.Instance.is_empty s then ctx
   else map_rel_context (fun x -> subst_instance_constr s x) ctx
 
-type id_key = pconstant tableKey
-let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y
+type id_key = constant tableKey
+let eq_id_key x y = Names.eq_table_key Constant.equal x y
-- 
cgit v1.2.3