diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 5 | ||||
| -rw-r--r-- | engine/universes.ml | 4 | ||||
| -rw-r--r-- | engine/universes.mli | 4 |
3 files changed, 8 insertions, 5 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 298302815a..04f55f2c35 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -609,7 +609,10 @@ let vars_of_global_reference env gr = [m] is appropriately lifted through abstractions of [t] *) let dependent_main noevar univs m t = - let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in + let eqc x y = + if univs then not (Option.is_empty (Universes.eq_constr_universes x y)) + else eq_constr_nounivs x y + in let rec deprec m t = if eqc m t then raise Occur diff --git a/engine/universes.ml b/engine/universes.ml index 0573dd2c60..6720fcef8f 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -199,7 +199,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = if res then Some !cstrs else None let test_constr_universes leq m n = - if m == n then true, Constraints.empty + if m == n then Some Constraints.empty else let cstrs = ref Constraints.empty in let eq_universes strict l l' = @@ -229,7 +229,7 @@ let test_constr_universes leq m n = else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs + if res then Some !cstrs else None let eq_constr_universes m n = test_constr_universes false m n let leq_constr_universes m n = test_constr_universes true m n diff --git a/engine/universes.mli b/engine/universes.mli index 0aeea91cdc..725c21d296 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]. *) |