From 15999903f875f4b5dbb3d5240d2ca39acc3cd777 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 26 May 2014 13:58:56 +0200
Subject: - Fix in kernel conversion not folding the universe constraints
 correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints,
 that would otherwise allow constraints that make a universe lower than Prop.
 - Fix stm/lemmas that was pushing constraints to the global context, it is
 done depending on the constant/variable polymorphic status now. - Adapt
 generalized rewriting in Type code to these fixes.

---
 dev/base_include   | 1 -
 dev/printers.mllib | 1 -
 2 files changed, 2 deletions(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index fa6add7d36..6e10dac3f9 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -155,7 +155,6 @@ open Command
 open Indschemes
 open Ind_tables
 open Auto_ind_decl
-(* open Lemmas *)
 open Coqinit
 open Coqtop
 open Discharge
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 5a9acb6dd4..2eae9d5985 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -194,4 +194,3 @@ Discharge
 Declare
 Ind_tables
 Top_printers
-
-- 
cgit v1.2.3