diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-19 13:36:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-26 14:56:24 +0100 |
| commit | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (patch) | |
| tree | e80f338121ea2f84d7978ef45d1adc310f308447 /pretyping/evarutil.ml | |
| parent | 36c6e9508a42d00686e90441999481354152aaa3 (diff) | |
More efficient implementation of equality-up-to-universes in Universes.
Instead of accumulating constraints which are not present in the original
graph, we parametrize the equality function by a function actually merging
those constraints in the current graph. This prevents doing the work twice.
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 508b9e802..3c3afac54 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -860,13 +860,14 @@ let kind_of_term_upto sigma t = let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in - let b, c = + let fold cstr sigma = + try Some (add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | UniversesDiffer -> None + in + let ans = Universes.eq_constr_univs_infer_with (fun t -> kind_of_term_upto sigma1 t) (fun u -> kind_of_term_upto sigma2 u) - (universes sigma2) t u + (universes sigma2) fold t u sigma2 in - if b then - try let _ = add_universe_constraints sigma2 c in true - with Univ.UniverseInconsistency _ | UniversesDiffer -> false - else false + match ans with None -> false | Some _ -> true |