diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-27 23:59:05 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-28 16:57:55 +0100 |
| commit | 90dfacaacfec8265b11dc9291de9510f515c0081 (patch) | |
| tree | 7cdf561c5f7a8df718152b37a2943776892f76e3 /kernel/reduction.ml | |
| parent | 9ce6802ea563437b15e45198f4d8d0f716a576bb (diff) | |
Conversion of polymorphic inductive types was incomplete in VM and native.
Was showing up when comparing e.g. prod Type Type with prod Type Type (!) with
a polymorphic prod.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2c111a55b..892557ac6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -173,7 +173,7 @@ let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare @@ -185,8 +185,10 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) -let convert_instances flex u u' (s, check) = - (check.compare_instances flex u u' s, check) +(* [flex] should be true for constants, false for inductive types and + constructors. *) +let convert_instances ~flex u u' (s, check) = + (check.compare_instances ~flex u u' s, check) let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else @@ -196,7 +198,7 @@ let conv_table_key infos k1 k2 cuniv = else let flex = evaluable_constant cst (info_env infos) && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst) - in convert_instances flex u u' cuniv + 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 @@ -590,7 +592,7 @@ let check_sort_cmp_universes env pb s0 s1 univs = let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs -let check_convert_instances _flex u u' univs = +let check_convert_instances ~flex u u' univs = if Univ.Instance.check_eq univs u u' then univs else raise NotConvertible @@ -630,7 +632,7 @@ let infer_cmp_universes env pb s0 s1 univs = | CONV -> infer_eq univs u1 u2) else univs -let infer_convert_instances flex u u' (univs,cstrs) = +let infer_convert_instances ~flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare = |