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.

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8ed8f18566..8fe0a68933 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1286,7 +1286,6 @@ let specialize (c,lbind) g =
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
       let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
-      let nargs = List.length tstack in
       let rec chk = function
       | [] -> []
       | t::l -> if occur_meta t then [] else t :: chk l
-- 
cgit v1.2.3