diff options
| author | Maxime Dénès | 2017-12-20 00:36:22 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-20 00:36:22 +0100 |
| commit | 7fac7294a1906a8df835e6d7be5bb1bca3f727b5 (patch) | |
| tree | d6e8a1997b71784d26880ca818ca4280b8ac39e0 /kernel | |
| parent | 5193624aadcbac71487e0c045060d8b4b61126b3 (diff) | |
| parent | cf81bf01602ef5ab725b604f5c243a83adf8d31c (diff) | |
Merge PR #6468: Fix order of let-in representation comment.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 21c477578c..98bf713082 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: |