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 /plugins/btauto/refl_btauto.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 'plugins/btauto/refl_btauto.ml')
0 files changed, 0 insertions, 0 deletions