diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.mli | 8 |
2 files changed, 8 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6c664f7918..1ae89347ad 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -316,7 +316,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let cuniv = conv_table_key infos fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with NotConvertible -> + with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in let (app1,app2) = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9812c45f7b..8a2b2469d6 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 |