diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-26 15:02:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-26 15:02:05 +0000 |
| commit | 8b4f27559be5e1155f04e6c0b5e205caffdffcb8 (patch) | |
| tree | 44319b79e51ae6005a55a8f9974651d5d40ea05b /kernel/term.mli | |
| parent | daf4ef5bb4138eb2ab9b7bf39d1c6a08984b8c01 (diff) | |
MAJ commentaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@282 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index ab1db881a..a43012a0f 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -343,19 +343,19 @@ val appvect : constr * constr array -> constr val appvectc : constr -> constr array -> constr (* [prodn n l b] = $(x_1:T_1)..(x_n:T_n)b$ - where $l = [(x_1,T_1);\dots;(x_n,T_n);Gamma]$ *) + where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *) val prodn : int -> (name * constr) list -> constr -> constr (* [lamn n l b] = $[x_1:T_1]..[x_n:T_n]b$ - where $l = [(x_1,T_1);\dots;(x_n,T_n);Gamma]$ *) + where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *) val lamn : int -> (name * constr) list -> constr -> constr (* [prod_it b l] = $(x_1:T_1)..(x_n:T_n)b$ - where $l = [x_1:T_1;..x_n:T_n]$ *) + where $l = [(x_n,T_n);\dots;(x_1,T_1)]$ *) val prod_it : constr -> (name * constr) list -> constr (* [lam_it b l] = $[x_1:T_1]..[x_n:T_n]b$ - where $l = [x_1:T_1;..;x_n:T_n]$ *) + where $l = [(x_n,T_n);\dots;(x_1,T_1)]$ *) val lam_it : constr -> (name * constr) list -> constr (* [to_lambda n l] |