diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-06 16:30:06 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-06 16:30:06 +0200 |
| commit | 036a8660f11178a2523982d109ba11b99c062a3d (patch) | |
| tree | b81de584d2c54fca18859c74922798e7e433cb17 /pretyping | |
| parent | 600c258adee5d6e91e855ff73c58b922d48f444e (diff) | |
Fix #5539: algebraic universe produced by cases.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 73be9d6b7..c5a4b4ff0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1845,7 +1845,7 @@ let build_inversion_problem loc env sigma tms t = (* [pb] is the auxiliary pattern-matching serving as skeleton for the return type of the original problem Xi *) let s' = Retyping.get_sort_of env sigma t in - let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in + let sigma, s = Evd.new_sort_variable univ_flexible sigma in let sigma = Evd.set_leq_sort env sigma s' s in let evdref = ref sigma in let pb = |