diff options
| author | herbelin | 2007-05-23 10:29:01 +0000 |
|---|---|---|
| committer | herbelin | 2007-05-23 10:29:01 +0000 |
| commit | b483e1732682bd1b8cec8d5d3a600c93d90f44ab (patch) | |
| tree | 73061a8da273c859530bbf90b61e8f9ad01ccb34 /kernel | |
| parent | 500aaf4e5ab37550efc0e0493b0afa45eaf250d3 (diff) | |
Suite restructuration unification et division des problèmes
d'unification des types des with-bindings en deux: les problèmes
d'unification susceptibles d'introduire une coercion sont retardés
(comme dans le commit r9850) et ceux susceptibles de fournir d'autres
instances restent faits au plus tôt (comme avant le commit r9850).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9851 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 4 | ||||
| -rw-r--r-- | kernel/term.mli | 1 |
2 files changed, 4 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 3386f45f51..5f9a3ff93d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -388,7 +388,9 @@ let destApplication = destApp let isApp c = match kind_of_term c with App _ -> true | _ -> false -let isProd c = match kind_of_term c with | Prod(_) -> true | _ -> false +let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false + +let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false (* Destructs a constant *) let destConst c = match kind_of_term c with diff --git a/kernel/term.mli b/kernel/term.mli index 4133ca8920..fcae3341e4 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -234,6 +234,7 @@ val isMeta : constr -> bool val isSort : constr -> bool val isCast : constr -> bool val isApp : constr -> bool +val isLambda : constr -> bool val isProd : constr -> bool val isConst : constr -> bool val isConstruct : constr -> bool |