diff options
| -rw-r--r-- | kernel/univ.ml | 8 | ||||
| -rw-r--r-- | kernel/univ.mli | 4 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 19 |
3 files changed, 15 insertions, 16 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 1aad0fce1..0193542a3 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -801,6 +801,14 @@ let no_upper_constraints u cst = | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst | Max _ -> anomaly "no_upper_constraints" +(* Is u mentionned in v (or equals to v) ? *) + +let univ_depends u v = + match u, v with + | Atom u, Atom v -> u = v + | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl + | _ -> anomaly "univ_depends given a non-atomic 1st arg" + (* Pretty-printing *) let pr_arc = function diff --git a/kernel/univ.mli b/kernel/univ.mli index 8b3f62910..e4e66915d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -91,6 +91,10 @@ val subst_large_constraints : val no_upper_constraints : universe -> constraints -> bool +(** Is u mentionned in v (or equals to v) ? *) + +val univ_depends : universe -> universe -> bool + (** {6 Pretty-printing of universes. } *) val pr_uni_level : universe_level -> Pp.std_ppcmds diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index f0e643f5a..da316fd63 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -403,21 +403,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. *) @@ -429,7 +414,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 *) |