From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 kernel/term.ml | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index c920c80b..1f3d2635 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 10859 2008-04-27 16:46:15Z herbelin $ *)
+(* $Id: term.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
@@ -370,16 +370,22 @@ let destProd c = match kind_of_term c with
   | Prod (x,t1,t2) -> (x,t1,t2) 
   | _ -> invalid_arg "destProd"
 
+let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
+
 (* Destructs the abstraction [x:t1]t2 *)
 let destLambda c = match kind_of_term c with 
   | Lambda (x,t1,t2) -> (x,t1,t2) 
   | _ -> invalid_arg "destLambda"
 
+let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
+
 (* Destructs the let [x:=b:t1]t2 *)
 let destLetIn c = match kind_of_term c with 
   | LetIn (x,b,t1,t2) -> (x,b,t1,t2) 
   | _ -> invalid_arg "destProd"
 
+let isLetIn c =  match kind_of_term c with LetIn _ -> true | _ -> false
+
 (* Destructs an application *)
 let destApp c = match kind_of_term c with
   | App (f,a) -> (f, a)
@@ -389,10 +395,6 @@ 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 isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
-
 (* Destructs a constant *)
 let destConst c = match kind_of_term c with
   | Const kn -> kn
@@ -419,22 +421,27 @@ let destConstruct c = match kind_of_term c with
   | Construct (kn, a as r) -> r
   | _ -> invalid_arg "dest"
 
-let isConstruct c = match kind_of_term c with
-    Construct _ -> true | _ -> false
+let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 let destCase c = match kind_of_term c with
   | Case (ci,p,c,v) -> (ci,p,c,v)
   | _ -> anomaly "destCase"
 
+let isCase c =  match kind_of_term c with Case _ -> true | _ -> false
+
 let destFix c = match kind_of_term c with 
   | Fix fix -> fix
   | _ -> invalid_arg "destFix"
-	
+
+let isFix c =  match kind_of_term c with Fix _ -> true | _ -> false
+
 let destCoFix c = match kind_of_term c with 
   | CoFix cofix -> cofix
   | _ -> invalid_arg "destCoFix"
 
+let isCoFix c =  match kind_of_term c with CoFix _ -> true | _ -> false
+
 (******************************************************************)
 (* Cast management                                                *)
 (******************************************************************)
-- 
cgit v1.2.3