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.mli | |
| 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.mli')
| -rw-r--r-- | kernel/reduction.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index c3cc7b2b6..0df26d627 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -37,7 +37,7 @@ type conv_pb = CONV | CUMUL type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: bool (* Instance of a flexible constant? *) -> + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } @@ -50,6 +50,11 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(* [flex] should be true for constants, false for inductive types and +constructors. *) +val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> + 'a * 'a universe_compare -> 'a * 'a universe_compare + val checked_universes : Univ.universes universe_compare val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare |