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 8131753fe..dab1d2cea 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -405,7 +405,7 @@ val mkCoFix : cofixpoint -> constr
(** {6 Aliases} *)
val eq_constr : constr -> constr -> bool
-(** Alias for [Constr.eq] *)
+(** Alias for [Constr.equal] *)
val kind_of_term : constr -> (constr, types) kind_of_term
(** Alias for [Constr.kind] *)