diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-01 15:58:25 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-01 15:58:25 +0200 |
| commit | 11c1d469fc12e617d0840700bc01caf2a1d5276c (patch) | |
| tree | 508765dc8362b8a8cc31a82a6637c0057b7fdfaa /pretyping/reductionops.ml | |
| parent | 52ff7a60c23ad31a7e0eb9b0bdb5b7c7c23162f3 (diff) | |
| parent | e22796a610853d8e7ff64785c98004d8ceac98e3 (diff) | |
Merge PR#670: Postponing of universe constraints unification in term equality.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e7c963582..5a2328aaa 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1317,19 +1317,23 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) + let open Universes in let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in try - let fold cstr sigma = - try Some (Evd.add_universe_constraints sigma cstr) - with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None - in + let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in let b, sigma = let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty else - Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + in + let ans = match ans with + | None -> None + | Some cstr -> + try Some (Evd.add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with | None -> false, sigma |