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 | |
| 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')
| -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 298302815..04f55f2c3 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 0573dd2c6..6720fcef8 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 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]. *) |