From b09db5eaf922f2278d8fb94503f83728f41414a5 Mon Sep 17 00:00:00 2001
From: coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 16 Feb 2006 10:42:18 +0000
Subject: added isProd to term.mli. added elim_scheme to tactics.mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8049 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml  | 2 ++
 kernel/term.mli | 1 +
 2 files changed, 3 insertions(+)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index f83e69fcf..e83c32821 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -390,6 +390,8 @@ 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
+
 (* Destructs a constant *)
 let destConst c = match kind_of_term c with
   | Const kn -> kn
diff --git a/kernel/term.mli b/kernel/term.mli
index c0c57959f..160ef767b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -236,6 +236,7 @@ val isMeta : constr -> bool
 val isSort : constr -> bool
 val isCast : constr -> bool
 val isApp : constr -> bool
+val isProd : constr -> bool
 val isConst : constr -> bool
 val isConstruct : constr -> bool
 
-- 
cgit v1.2.3