aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.mli')
-rw-r--r--kernel/term.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/term.mli b/kernel/term.mli
index 008cad9947..c40b6142af 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -354,6 +354,9 @@ val for_all_named_declaration :
val for_all_rel_declaration :
(constr -> bool) -> rel_declaration -> bool
+val eq_named_declaration :
+ named_declaration -> named_declaration -> bool
+
(** {6 Contexts of declarations referred to by de Bruijn indices } *)
(** In [rel_context], more recent declaration is on top *)