diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 123c610166..21ed8e0a23 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -1362,25 +1362,23 @@ let sigma_compare_instances ~flex i0 i1 sigma = raise Reduction.NotConvertible let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) + let len_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) in let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && - (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + 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.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx) + 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.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx) - in + let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in Univ.Constraint.union comp_cst comp_cst' | Reduction.CUMUL -> comp_cst in |