diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-23 10:29:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-23 10:29:01 +0000 |
| commit | b483e1732682bd1b8cec8d5d3a600c93d90f44ab (patch) | |
| tree | 73061a8da273c859530bbf90b61e8f9ad01ccb34 /kernel/term.mli | |
| 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/term.mli')
| -rw-r--r-- | kernel/term.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 4133ca892..fcae3341e 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 |