diff options
| author | letouzey | 2012-03-01 18:59:04 +0000 |
|---|---|---|
| committer | letouzey | 2012-03-01 18:59:04 +0000 |
| commit | 15cb1aace0460e614e8af1269d874dfc296687b0 (patch) | |
| tree | 87f3c4237d3ef3dd9b34af8a4c8f2772f470243d /pretyping | |
| parent | 70d8c1e7a24b542c8e3f1788fd18226e2469801b (diff) | |
Univ: a univ_depends function to avoid a hack in Inductiveops
univ_depends checks whether a universe variable appears or
is equal to a universe. In comparison with the previous hack
in inductiveops based on try...catching UniverseInconsistency,
this should be semantically equivalent, simplier, and more
robust in case we allow someday an unsafe mode where
merge_constraints would be a no-op.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 19 |
1 files changed, 3 insertions, 16 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index f0e643f5ab..da316fd63c 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 *) |