From ead5d80dff08f97998e81acfb2562dde741a26af Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 3 Aug 2014 23:19:56 +0200 Subject: 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. --- kernel/reduction.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'kernel/reduction.ml') 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 -- cgit v1.2.3