aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.mli')
-rw-r--r--kernel/term.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index ba521978e..7cb3b662d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -477,7 +477,7 @@ val iter_constr_with_binders :
('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
[@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"]
-val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool
[@@ocaml.deprecated "Alias for [Constr.compare_head]"]
type constr = Constr.constr