From 4b0f28073b3db03d1991c680be99aedbb45de225 Mon Sep 17 00:00:00 2001
From: corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 25 Nov 2003 12:18:36 +0000
Subject: CC: added injection theory

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

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 472ffb2c8..785afb0d4 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -367,7 +367,9 @@ val to_lambda : int -> constr -> constr
 val to_prod : int -> constr -> constr
 
 (* pseudo-reduction rule *)
-(* [prod_applist] $(x1:B1;...;xn:Bn)B a1...an \rightarrow B[a1...an]$ *)
+
+(* [prod_appvect] $(x1:B1;...;xn:Bn)B a1...an \rightarrow B[a1...an]$ *)
+val prod_appvect : constr -> constr array -> constr
 val prod_applist : constr -> constr list -> constr
 
 (*s Other term destructors. *)
-- 
cgit v1.2.3