diff options
| author | Gaëtan Gilbert | 2018-02-20 00:27:40 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-09 16:29:06 +0100 |
| commit | db0918bfa5089f9ab44374504cbd0ddc758ea1e5 (patch) | |
| tree | 5b68a2bd48fc961987a193f4361c46f7b9940b33 /kernel/reduction.mli | |
| parent | 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (diff) | |
Cumulativity: improve treatment of irrelevant universes.
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ad52c93f62..14e4270b7c 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -41,7 +41,8 @@ type 'a universe_compare = { (* Might raise NotConvertible *) compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a } + compare_cumul_instances : conv_pb -> Univ.Variance.t array -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } type 'a universe_state = 'a * 'a universe_compare @@ -49,7 +50,7 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t -val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t -> +val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int |