From b483e1732682bd1b8cec8d5d3a600c93d90f44ab Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 23 May 2007 10:29:01 +0000
Subject: 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
---
 kernel/term.ml  | 4 +++-
 kernel/term.mli | 1 +
 2 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3