diff options
| author | herbelin | 2012-03-20 08:02:11 +0000 |
|---|---|---|
| committer | herbelin | 2012-03-20 08:02:11 +0000 |
| commit | 541ff113562c62381100caea84bf58ce5b2cd3ce (patch) | |
| tree | 5e194ce12f2a98843bb0a39818715838e1905bd7 /kernel | |
| parent | 0a59c2e537040d3e74fd65cd738fa617cbd4f1e2 (diff) | |
Reorganizing the structure of evarutil.ml (only restructuration, no
change of semantics).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 1 | ||||
| -rw-r--r-- | kernel/term.mli | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 0a4782d8c1..ab676f0e9a 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -323,6 +323,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 diff --git a/kernel/term.mli b/kernel/term.mli index a54130efa2..e83be6d63b 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -229,8 +229,9 @@ val kind_of_type : types -> (constr, types) kind_of_type (** {6 Simple term case analysis. } *) val isRel : constr -> bool +val isRelN : int -> constr -> bool val isVar : constr -> bool -val isVarId : identifier -> constr -> bool +val isVarId : identifier -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool |