From 97c848795c1c26e6413737e9b8150eb9335946ed Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Dec 2011 18:55:42 +0000
Subject: Some extra universe refreshing seems needed in abstract_generalize
 (for generalize_eqs).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14792 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 45eee91eef..1b35888c03 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2411,6 +2411,7 @@ let abstract_args gl generalize_vars dep id defined f args =
     in
     let argty = pf_type_of gl arg in
     let argty = refresh_universes_strict argty in 
+    let ty = refresh_universes_strict ty in
     let lenctx = List.length ctx in
     let liftargty = lift lenctx argty in
     let leq = constr_cmp Reduction.CUMUL liftargty ty in
-- 
cgit v1.2.3