diff options
| author | Maxime Dénès | 2017-07-13 15:05:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-13 15:05:48 +0200 |
| commit | e3eb17a728d7b6874e67462e8a83fac436441872 (patch) | |
| tree | c7932e27be16f4d2c20da8d61c3a61b101be7f70 /kernel/reduction.ml | |
| parent | 9427b99b167842bc4a831def815c4824030d518f (diff) | |
| parent | 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 (diff) | |
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index de4efbba93..2bf9f43a5a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -680,8 +680,7 @@ let infer_check_conv_constructors let check_inductive_instances cv_pb cumi u u' univs = let length_ind_instance = - Univ.Instance.length - (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((length_ind_instance = Univ.Instance.length u) && @@ -690,16 +689,14 @@ let check_inductive_instances cv_pb cumi u u' univs = else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.UContext.constraints - (Univ.subst_instance_context comp_subst ind_subtypctx) + Univ.AUContext.instantiate comp_subst ind_subtypctx in let comp_cst = match cv_pb with CONV -> let comp_cst' = let comp_subst = (Univ.Instance.append u' u) in - Univ.UContext.constraints - (Univ.subst_instance_context comp_subst ind_subtypctx) + Univ.AUContext.instantiate comp_subst ind_subtypctx in Univ.Constraint.union comp_cst comp_cst' | CUMUL -> comp_cst @@ -767,8 +764,7 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = let length_ind_instance = - Univ.Instance.length - (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in if not ((length_ind_instance = Univ.Instance.length u) && @@ -777,16 +773,15 @@ let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.UContext.constraints - (Univ.subst_instance_context comp_subst ind_subtypctx) + Univ.AUContext.instantiate comp_subst ind_subtypctx in let comp_cst = match cv_pb with CONV -> let comp_cst' = let comp_subst = (Univ.Instance.append u' u) in - Univ.UContext.constraints - (Univ.subst_instance_context comp_subst ind_subtypctx) in + Univ.AUContext.instantiate comp_subst ind_subtypctx + in Univ.Constraint.union comp_cst comp_cst' | CUMUL -> comp_cst in |