From 66b0c04d4799c023504fe847a4b7b341dcbe92ac Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 7 Oct 2008 13:27:55 +0000
Subject: fixing r11433 again: - backtrack on kernel modifications: the
 monomorphic instance of an inductive   type is constrained to live in an
 universe higher (or equal) than all the   instances - improved support for
 polymorphic inductive types at the refiner level:   introduced
 type_of_inductive_knowing_conclusion that computes the   instance to match
 the current conclusion universe.

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 15f8b8a731..eb879d977a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -237,12 +237,6 @@ let check_conv_leq_goal env sigma arg ty conclty =
 let goal_type_of env sigma c =
   (if !check then type_of else Retyping.get_type_of) env sigma c
 
-let refresh_poly_universes c =
-  let (ctx,t) = decompose_prod_assum c in
-  let ctx' = List.map (fun (na,b,ty) -> (na,b,refresh_universes ty)) ctx in
-  let t' = refresh_universes t in
-  it_mkProd_or_LetIn t' ctx'
-
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = evar_env goal in
   let hyps = goal.evar_hyps in
@@ -272,8 +266,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 		when (isInd f or has_polymorphic_type (destConst f)) ->
 		(* Sort-polymorphism of definition and inductive types *)
 		goalacc, 
-		refresh_poly_universes
-                  (type_of_global_reference_knowing_parameters env sigma f [||])
+                type_of_global_reference_knowing_conclusion env sigma f conclty
 	    | _ -> 
 		mk_hdgoals sigma goal goalacc f
 	in
-- 
cgit v1.2.3