From d18d82c9e58567384ea632c77a5c1531f6d534cb Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 20 Oct 1999 20:41:08 +0000
Subject:  - documentation repertoire proofs/  - IsAppL of constr * constr list
 ==> répercussion  - module Clenv (suite; as terminé)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 1fa03507f..511361241 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -75,7 +75,7 @@ type kindOfTerm =
   | IsCast         of constr * constr
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
-  | IsAppL         of constr array
+  | IsAppL         of constr * constr list
   | IsConst        of section_path * constr array
   | IsAbst         of section_path * constr array
   | IsEvar         of int * constr array
@@ -146,7 +146,7 @@ val mkNamedLambda : identifier -> constr -> constr -> constr
 (* If $a = [| t_1; \dots; t_n |]$, constructs the application 
    $(t_1~\dots~t_n)$. *)
 val mkAppL : constr array -> constr
-val mkAppList : constr list  -> constr
+val mkAppList : constr -> constr list  -> constr
 
 (* Constructs a constant *) 
 (* The array of terms correspond to the variables introduced in the section *)
-- 
cgit v1.2.3