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.mli | |
| 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.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 918ba12f0f..9ee815ebc0 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,8 +34,12 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : ?status:Evd.rigid -> - ?onlyalg:bool (* Only algebraic universes *) -> +val refresh_universes : + ?status:Evd.rigid -> + ?onlyalg:bool (* Only algebraic universes *) -> + ?propset:bool -> + (* Also refresh Prop and Set universes, so that the returned type can be any supertype + of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types |