diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-24 15:13:47 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-26 14:16:26 +0200 |
| commit | d8176e6baaa33692ed82b9ac3c6e57e85f51dff0 (patch) | |
| tree | 220abe1095acdff596bbf89b31decd67df11270b /kernel/reduction.ml | |
| parent | 13deafee96893a5ec332ad221469e3e5460693f1 (diff) | |
Update infer_conv to record trivial Prop <= Type i constraints that are needed during
unification.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5f0684d37..8773f4f34 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -661,11 +661,11 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = v2 let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = - let b = - if cv_pb == CUMUL then leq_constr_univs univs t1 t2 - else eq_constr_univs univs t1 t2 + let b, cstrs = + if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 + else Constr.eq_constr_univs_infer univs t1 t2 in - if b then Constraint.empty + if b && Univ.check_constraints cstrs univs then cstrs else let (u, cstrs) = clos_fconv reds cv_pb l2r evars env (univs, Some Constraint.empty) t1 t2 |