From 7002b3daca6da29eadf80019847630b8583c3daf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 3 Aug 2014 20:02:49 +0200
Subject: Move to a representation of universe polymorphic constants using
 indices for variables. Simplifies instantiation of constants/inductives,
 requiring less allocation and Map.find's. Abstraction by variables is handled
 mostly inside the kernel but could be moved outside.

---
 kernel/safe_typing.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0578d35fc9..71a6b7a399 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -363,15 +363,6 @@ let constraints_of_sfb sfb =
   | SFBmodtype mtb -> [Now mtb.typ_constraints]
   | SFBmodule mb -> [Now mb.mod_constraints]
 
-(* let add_constraints cst senv = *)
-(*   { senv with *)
-(*     env = Environ.add_constraints cst senv.env; *)
-(*     univ = Univ.Constraint.union cst senv.univ } *)
-
-(* let next_universe senv = *)
-(*   let univ = senv.max_univ in *)
-(*     univ + 1, { senv with max_univ = univ + 1 } *)
-
 (** A generic function for adding a new field in a same environment.
     It also performs the corresponding [add_constraints]. *)
 
-- 
cgit v1.2.3