diff options
| author | Pierre-Marie Pédrot | 2017-05-12 15:16:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-23 10:22:22 +0200 |
| commit | e22796a610853d8e7ff64785c98004d8ceac98e3 (patch) | |
| tree | 9fa94a7cbbfb08f001a065f44542180da23e5f53 | |
| parent | bf84180f963a31d1ec850d4ccedd599f2984ea9b (diff) | |
Postponing of universe constraints unification in term equality.
Instead of calling the universe unification at each term node, we accumulate
them and try to perform unification at the very end. This seems to be
experimentally faster.
| -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 52f424f751..dcb19b31af 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 |