From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- pretyping/inductiveops.ml | 19 +++---------------- 1 file changed, 3 insertions(+), 16 deletions(-) (limited to 'pretyping/inductiveops.ml') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 15fd226f..0b59fc40 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -392,21 +392,6 @@ let arity_of_case_predicate env (ind,params) dep k = (* Inferring the sort of parameters of a polymorphic inductive type knowing the sort of the conclusion *) -(* Check if u (sort of a parameter) appears in the sort of the - inductive (is). This is done by trying to enforce u > u' >= is - in the empty univ graph. If an inconsistency appears, then - is depends on u. *) -let is_constrained is u = - try - let u' = fresh_local_univ() in - let _ = - merge_constraints - (enforce_geq u (super u') - (enforce_geq u' is empty_constraint)) - initial_universes in - false - with UniverseInconsistency _ -> true - (* Compute the inductive argument types: replace the sorts that appear in the type of the inductive by the sort of the conclusion, and the other ones by fresh universes. *) @@ -418,7 +403,9 @@ let rec instantiate_universes env scl is = function | (na,None,ty)::sign, Some u::exp -> let ctx,_ = Reduction.dest_arity env ty in let s = - if is_constrained is u then + (* Does the sort of parameter [u] appear in (or equal) + the sort of inductive [is] ? *) + if univ_depends u is then scl (* constrained sort: replace by scl *) else (* unconstriained sort: replace by fresh universe *) -- cgit v1.2.3