aboutsummaryrefslogtreecommitdiffhomepage
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, 1 insertions, 1 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cf6ba07c6..48704f75b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -397,7 +397,7 @@ type clbinding =
(** Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * env * constr * constr
-val add_conv_pb : evar_constraint -> evar_map -> evar_map
+val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
val extract_changed_conv_pbs : evar_map ->
(Evar.Set.t -> evar_constraint -> bool) ->