From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- kernel/term.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/term.ml') 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 -- cgit v1.2.3