diff options
| author | Matthieu Sozeau | 2014-08-03 23:19:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-03 23:39:02 +0200 |
| commit | ead5d80dff08f97998e81acfb2562dde741a26af (patch) | |
| tree | 7b5ad21993d0c1625f6609eba0e385378ca43faf /kernel | |
| parent | ef72be87579be34e9454fe1f785ff36a9c25246c (diff) | |
Fix infer conv using the wrong universe conversion flexibility information
for constants that are not unfolded during conversion.
Fix discharge of polymorphic section variables over inductive types.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 28fe7141ff..78d2105ab0 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -199,8 +199,9 @@ let conv_table_key infos k1 k2 cuniv = | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' -> if Univ.Instance.equal u u' then cuniv else - let flex = evaluable_constant cst (info_env infos) in - convert_instances flex u u' cuniv + let flex = evaluable_constant cst (info_env infos) + && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst) + in convert_instances flex u u' cuniv | VarKey id, VarKey id' when Id.equal id id' -> cuniv | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible |