aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r--pretyping/evd.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 3d796d423f..a5ff11c7ed 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -281,8 +281,6 @@ type clbinding =
| Cltyp of Name.t * constr freelisted
| Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
-val map_clb : (constr -> constr) -> clbinding -> clbinding
-
(** Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * env * constr * constr