aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.mli
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-11 11:35:17 +0100
committerMaxime Dénès2017-12-11 11:35:17 +0100
commita77f3a3e076e273af35ad520cae2eef0e3552811 (patch)
treebedea2242a6c3f0e2deb6a2cd4f731f7c5014824 /pretyping/reductionops.mli
parent5aaa240e4480ade7a5348e71a95fe3b2bc5a2c4e (diff)
parent611da26d847888031cac4d6976b9e7e1e90cdc0e (diff)
Merge PR #6368: [api] Remove yet another type alias.
Diffstat (limited to 'pretyping/reductionops.mli')
-rw-r--r--pretyping/reductionops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 34fdbe8583..7e12d263aa 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -260,7 +260,7 @@ val is_transparent : Environ.env -> Constant.t tableKey -> bool
(** {6 Conversion Functions (uses closures, lazy strategy) } *)
-type conversion_test = constraints -> constraints
+type conversion_test = Constraint.t -> Constraint.t
val pb_is_equal : conv_pb -> bool
val pb_equal : conv_pb -> conv_pb