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 | |
| 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.
| -rw-r--r-- | kernel/reduction.ml | 5 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 1 |
2 files changed, 4 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 diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 971ae70d86..9de0edea81 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -101,6 +101,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mib.mind_packets in let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in + let abs_ctx = Univ.instantiate_univ_context abs_ctx in let univs = Univ.UContext.union abs_ctx univs in let record = match mib.mind_record with | None -> None |