diff options
| author | Pierre-Marie Pédrot | 2020-10-11 17:50:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-11 17:56:44 +0200 |
| commit | 7320cd84f92793572550d1fe1a2181f40466fa81 (patch) | |
| tree | 69496a726a61f7d047e9260b9e4b6dc36ca05d4d /kernel/reduction.ml | |
| parent | eb5a67de1fc586acc588d5c61c84df670284f054 (diff) | |
Similarly remove the explicit graph argument in the ~evar conversion API.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 6 |
1 files changed, 3 insertions, 3 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 |