diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-11-28 18:36:10 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-30 15:43:12 +0100 |
| commit | d06211803146dec998b414d215d4d93190e2001f (patch) | |
| tree | 6847ddc614130284e0e83e465496cfbbd63daed3 /kernel/reduction.mli | |
| parent | a27ac0315dcbb99c64a260bac3988199a26b39cf (diff) | |
Univs: fix bug #5180
In the kernel's generic conversion, backtrack on UniverseInconsistency
for the unfolding heuristic (single backtracking point in reduction).
This exception can be raised in the univ_compare structure to produce
better error messages when the generic conversion function is called
from higher level code in reductionops.ml, which itself is called during
unification in evarconv.ml.
Inside the kernel, the infer and check variants of conversion never
raise UniverseInconsistency though, so this does not change the behavior
of the kernel.
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9812c45f7..8a2b2469d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,7 +36,7 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL type 'a universe_compare = - { (* Might raise NotConvertible *) + { (* Might raise NotConvertible or UnivInconsistency *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; @@ -56,9 +56,12 @@ constructors. *) val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(** These two never raise UnivInconsistency, inferred_universes + just gathers the constraints. *) val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare +(** These two functions can only raise NotConvertible *) val conv : constr extended_conversion_function val conv_leq : types extended_conversion_function @@ -70,6 +73,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function +(** Depending on the universe state functions, this might raise + [UniverseInconsistency] in addition to [NotConvertible] (for better error + messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function |