- 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.

1 files changed, 0 insertions, 1 deletions

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