diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2acf6bfe6..87f29ba49 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -363,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 |