diff options
| -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 28fe7141f..78d2105ab 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 971ae70d8..9de0edea8 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 |