diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-15 22:32:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-15 22:32:31 +0200 |
| commit | 8c5d14bd399a02d15d46a27f14b7791afb30c3c5 (patch) | |
| tree | e3ed51bbd237cb341b70ee599b5cbd041f433cf7 /pretyping | |
| parent | cd3a834754449e9e554a4878ed5f318475434c38 (diff) | |
| parent | 36f3ae391ee188edb9d858d8832d7fd611db0482 (diff) | |
Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4fd030845..e8380136e 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -67,7 +67,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) else t | UnivFlexible alg -> if onlyalg && alg then - (evdref := Evd.make_flexible_variable !evdref false l; t) + (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) | Sort (Prop Pos as s) when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", |