diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-31 18:31:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-31 18:57:44 +0100 |
| commit | c48838c05eea1793c2d0a11292f8fc4eb784cd02 (patch) | |
| tree | 18ef4ff5dace16fa286ecf6c8479ff55aabfc453 /engine/universes.mli | |
| parent | d562d0e0ef9aab9d3f7333aec39172ed37d4d5ae (diff) | |
Stronger static invariant in equality upto universes.
We return an option type, as constraints were always dropped if the boolean
was false. They did not make much sense anyway.
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index 0aeea91cd..725c21d29 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -88,11 +88,11 @@ val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) -val eq_constr_universes : constr -> constr -> bool universe_constrained +val eq_constr_universes : constr -> constr -> universe_constraints option (** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) -val leq_constr_universes : constr -> constr -> bool universe_constrained +val leq_constr_universes : constr -> constr -> universe_constraints option (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) |