aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/context.mli')
-rw-r--r--kernel/context.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/context.mli b/kernel/context.mli
index 1d732d273..b7eb7a76a 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -115,3 +115,5 @@ val lookup_rel : int -> rel_context -> rel_declaration
val rel_context_length : rel_context -> int
(** Size of the [rel_context] without LetIns *)
val rel_context_nhyps : rel_context -> int
+(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
+val rel_context_tags : rel_context -> bool list