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.ml | |
| 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.ml')
| -rw-r--r-- | kernel/term.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 3386f45f5..5f9a3ff93 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 |