aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.mli
diff options
context:
space:
mode:
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