aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-10-11 17:50:40 +0200
committerPierre-Marie Pédrot2020-10-11 17:56:44 +0200
commit7320cd84f92793572550d1fe1a2181f40466fa81 (patch)
tree69496a726a61f7d047e9260b9e4b6dc36ca05d4d /kernel/reduction.mli
parenteb5a67de1fc586acc588d5c61c84df670284f054 (diff)
Similarly remove the explicit graph argument in the ~evar conversion API.
Diffstat (limited to 'kernel/reduction.mli')
-rw-r--r--kernel/reduction.mli2
1 files changed, 1 insertions, 1 deletions
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