diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 6 | ||||
| -rw-r--r-- | kernel/reduction.mli | 2 | ||||
| -rw-r--r-- | kernel/typeops.mli | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8258c1c086..96bf370342 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -189,7 +189,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit (* functions of this type can be called from outside the kernel *) type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> env -> - ?evars:((existential->constr option) * UGraph.t) -> + ?evars:(existential->constr option) -> 'a -> 'a -> unit exception NotConvertible @@ -888,8 +888,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = () (* Profiling *) -let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) = - let evars, univs = evars in +let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) = + let univs = Environ.universes env in if Flags.profile then let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 3c747f0ff8..7d32596f74 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,7 +31,7 @@ exception NotConvertible type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> env -> - ?evars:((existential->constr option) * UGraph.t) -> + ?evars:(existential->constr option) -> 'a -> 'a -> unit type conv_pb = CONV | CUMUL diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 87a5666fcc..d381e55dd6 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> +val check_hyps_inclusion : env -> ?evars:(existential->constr option) -> GlobRef.t -> Constr.named_context -> unit (** Types for primitives *) |