summaryrefslogtreecommitdiff
path: root/kernel/term.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term.ml')
-rw-r--r--kernel/term.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index dcb63cf7..46bc7c56 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -322,6 +322,7 @@ let isCast c = match kind_of_term c with Cast _ -> true | _ -> false
(* Tests if a de Bruijn index *)
let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
+let isRelN n c = match kind_of_term c with Rel n' -> n = n' | _ -> false
(* Tests if a variable *)
let isVar c = match kind_of_term c with Var _ -> true | _ -> false