diff options
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 0b605820d..6d8783d7e 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -166,16 +166,14 @@ let convert_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 |