diff options
| author | Pierre-Marie Pédrot | 2018-06-22 00:43:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:29:55 +0100 |
| commit | 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 (patch) | |
| tree | 9f54ad363b2c8f855be97860ba1900572353e164 /kernel/reduction.mli | |
| parent | ecfbeaa62f9d8bd4dc4600cf39df2262af718313 (diff) | |
Move transparent_state to its own module.
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 581e8bd88a..9b26e7b3dc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,7 +31,7 @@ exception NotConvertibleVect of int type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = - ?l2r:bool -> ?reds:Names.transparent_state -> env -> + ?l2r:bool -> ?reds:TranspState.t -> env -> ?evars:((existential->constr option) * UGraph.t) -> 'a -> 'a -> unit @@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:Names.transparent_state -> constr infer_conversion_function + ?ts:TranspState.t -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> - ?ts:Names.transparent_state -> types infer_conversion_function + ?ts:TranspState.t -> 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 + TranspState.t -> (constr,'a) generic_conversion_function val default_conv : conv_pb -> ?l2r:bool -> types kernel_conversion_function val default_conv_leq : ?l2r:bool -> types kernel_conversion_function |