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.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/term.mli')

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