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.ml | |
| 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.ml')
| -rw-r--r-- | engine/universes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |