From 943b5f9a9a90e856171f9dcb13ae56eaa8d87ef0 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 29 Oct 2013 19:47:14 +0000
Subject: Do not generate useless argument arrays in whd_* functions.

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

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index fa204b5701..44a10aa355 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -339,6 +339,11 @@ let decompose_app c =
     | App (f,cl) -> (f, Array.to_list cl)
     | _ -> (c,[])
 
+let decompose_appvect c =
+  match kind_of_term c with
+    | App (f,cl) -> (f, cl)
+    | _ -> (c,[||])
+
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index a3745d5e31..8131753fee 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -152,6 +152,9 @@ val destApplication : constr -> constr * constr array
 (** Decompose any term as an applicative term; the list of args can be empty *)
 val decompose_app : constr -> constr * constr list
 
+(** Same as [decompose_app], but returns an array. *)
+val decompose_appvect : constr -> constr * constr array
+
 (** Destructs a constant *)
 val destConst : constr -> constant
 
-- 
cgit v1.2.3