From de5631d1793834eb26f17f82d5e198b778008f64 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 Apr 2010 08:49:15 +0000
Subject: Fixed bug #2999 (destruct was not refreshing universes of what it
 generalized *) + changed printing of universe Type(0) to Set, so not to show
 that the implementation starts numbering with Set=Type(0) while documentation
 uses Type(0) for the common type of Prop and Set.

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 51aa86613e..41fab4e716 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2903,6 +2903,7 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
 let apply_induction_in_context hyp0 elim indvars names induct_tac gl =
   let env = pf_env gl in
   let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
+  let deps = List.map (on_pi3 refresh_universes_strict) deps in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let dephyps = List.map (fun (id,_,_) -> id) deps in
   let deps_cstr =
-- 
cgit v1.2.3