diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-07 15:09:27 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-10 01:34:19 +0100 |
| commit | 10d3d803e6b57024dd15df7d61670ce42260948a (patch) | |
| tree | 05745836a6d8b2c0a0dad517f42cd5932902c863 /pretyping/reductionops.ml | |
| parent | b641379bb1ce569e46f39e16736640a4223a5758 (diff) | |
[get_cumulativity_constraints] allowing further code sharing.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 30 |
1 files changed, 5 insertions, 25 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5ecaf0da1..418ea271c 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1324,31 +1324,11 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let len_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) - in - let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in - if not ((len_instance = Univ.Instance.length u) && - (len_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_sbctx - in - let comp_cst = - match cv_pb with - Reduction.CONV -> - let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in - Univ.Constraint.union comp_cst comp_cst' - | Reduction.CUMUL -> comp_cst - in - try Evd.add_constraints sigma comp_cst - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> - raise Reduction.NotConvertible +let sigma_check_inductive_instances csts sigma = + try Evd.add_constraints sigma csts + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = let open Reduction in |