diff options
| author | Pierre-Marie Pédrot | 2016-10-31 18:31:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-31 18:57:44 +0100 |
| commit | c48838c05eea1793c2d0a11292f8fc4eb784cd02 (patch) | |
| tree | 18ef4ff5dace16fa286ecf6c8479ff55aabfc453 /engine/termops.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/termops.ml')
| -rw-r--r-- | engine/termops.ml | 5 |
1 files changed, 4 insertions, 1 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 |