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 /pretyping/evarconv.ml | |
| parent | 9427b99b167842bc4a831def815c4824030d518f (diff) | |
| parent | 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 (diff) | |
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b5d195873c..87f29ba492 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -353,9 +353,8 @@ let exact_ise_stack2 env evd f sk1 sk2 = let check_leq_inductives evd cumi u u' = let u = EConstr.EInstance.kind evd u in let u' = EConstr.EInstance.kind evd u' in - let length_ind_instance = - Univ.Instance.length - (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + let length_ind_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in if not ((length_ind_instance = Univ.Instance.length u) && @@ -364,9 +363,7 @@ let check_leq_inductives evd cumi u u' = else begin let comp_subst = (Univ.Instance.append u u') in - let comp_cst = - Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst) - in + let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in Evd.add_constraints evd comp_cst end |