diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 12 | ||||
| -rw-r--r-- | kernel/term.mli | 8 |
2 files changed, 9 insertions, 11 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 411326106..a7ec0cfa1 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -596,13 +596,13 @@ let abs_implicit c = mkLambda Anonymous mkImplicit c let lambda_implicit a = mkLambda (Name(id_of_string"y")) mkImplicit a let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a) -(* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *) +(* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *) let prod_it = List.fold_left (fun c (n,t) -> mkProd n t c) -(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b with xn *) +(* lam_it b [xn:Tn;..;x1:T1] = [x1:T1]..[xn:Tn]b *) let lam_it = List.fold_left (fun c (n,t) -> mkLambda n t c) -(* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *) +(* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *) let prodn n env b = let rec prodrec = function | (0, env, b) -> b @@ -611,7 +611,7 @@ let prodn n env b = in prodrec (n,env,b) -(* lamn n ([x1:T1]..[xn:T]Gamma) b = [x1:T1]..[xn:Tn]b *) +(* lamn n [xn:Tn;..;x1:T1;Gamma] b = [x1:T1]..[xn:Tn]b *) let lamn n env b = let rec lamrec = function | (0, env, b) -> b @@ -668,9 +668,7 @@ let rec to_prod n lam = (* pseudo-reduction rule: * [prod_app s (Prod(_,B)) N --> B[N] - * with an strip_outer_cast on the first argument to produce a product. - * if this does not work, then we use the string S as part of our - * error message. *) + * with an strip_outer_cast on the first argument to produce a product *) let prod_app t n = match strip_outer_cast t with 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] |