diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 45 |
1 files changed, 29 insertions, 16 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2040acba7..123c61016 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1362,21 +1362,25 @@ 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.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + let ind_instance = + Univ.AUContext.instance (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 anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.subst_instance_constraints comp_subst ind_sbcst + Univ.UContext.constraints (Univ.subst_instance_context 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.subst_instance_constraints comp_subst ind_sbcst) in + let comp_cst' = + Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx) + in Univ.Constraint.union comp_cst comp_cst' | Reduction.CUMUL -> comp_cst in @@ -1389,34 +1393,43 @@ let sigma_conv_inductives cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = try sigma_compare_instances ~flex:false u1 u2 sigma with Reduction.NotConvertible -> - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> let num_param_arity = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs in if not (num_param_arity = sv1 && num_param_arity = sv2) then raise Reduction.NotConvertible else - let uinfind = mind.Declarations.mind_universes in - sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma - else raise Reduction.NotConvertible + sigma_check_inductive_instances cv_pb cumi u1 u2 sigma let sigma_conv_constructors (mind, ind, cns) u1 sv1 u2 sv2 sigma = try sigma_compare_instances ~flex:false u1 u2 sigma with Reduction.NotConvertible -> - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> let num_cnstr_args = let nparamsctxt = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in - nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + nparamsctxt + + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) in if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then raise Reduction.NotConvertible else - let uinfind = mind.Declarations.mind_universes in - sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma - else raise Reduction.NotConvertible + sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; |