From 51f5f4d37fdc3db1e7da951db11119bdb5a7554b Mon Sep 17 00:00:00 2001
From: glondu
Date: Mon, 8 Nov 2010 10:55:25 +0000
Subject: Refresh universes in params when generating schemes (Closes: #2429)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13631 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/indrec.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index acded3ac58..e1da61908a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -50,7 +50,11 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 (* Christine Paulin, 1996 *)
 
 let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
-  let lnamespar = mib.mind_params_ctxt in
+  let lnamespar = List.map
+    (fun (n, c, t) -> (n, c, Termops.refresh_universes t))
+    mib.mind_params_ctxt
+  in
+
   if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
-- 
cgit v1.2.3