From cf81bf01602ef5ab725b604f5c243a83adf8d31c Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Tue, 19 Dec 2017 14:08:58 +0900 Subject: Fix order of let-in representation comment. The comment had the type and value of the let-in swapped, which contradicted the listed types. --- kernel/constr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/constr.mli') diff --git a/kernel/constr.mli b/kernel/constr.mli index 21c477578..98bf71308 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -203,7 +203,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) - | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *) + | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:C := B in D"] is represented as [LetIn (A,B,C,D)]. *) | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])]. The {!mkApp} constructor also enforces the following invariant: -- cgit v1.2.3