diff options
| author | Matthieu Sozeau | 2016-05-09 17:40:04 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-04 15:48:15 +0200 |
| commit | a5b631f7260e7d29defd8bd5c67db543742c9ecd (patch) | |
| tree | ae3ccf9bcc9d46319abc3694415629487dd089c7 /pretyping/evarsolve.ml | |
| parent | 2ce64cc3124d30dbd42324c345cec378ccd66106 (diff) | |
congruence/univs: properly refresh (fix #4609)
In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 29af199a1e..c2d47790d5 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,7 +47,8 @@ let refresh_level evd s = | None -> true | Some l -> not (Evd.is_flexible_level evd l) -let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = +let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false) + pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh status dir t = @@ -62,6 +63,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' + | Sort (Prop _ as s) when propset && not dir -> + let s' = evd_comb0 (new_sort_variable status) evdref in + let evd = set_leq_sort env !evdref s s' in + modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> mkProd (na,u,refresh status dir v) | _ -> t |