typo in reference manual 1.2.12

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2962
From: office@aha66.at
Reported version: 8.4
CC: @letouzey

[coqbot]

Comment author: office@aha66.at

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual003.html

AFTER

1.2.12 Local definitions (let-in)

let ident := term1 in term2 denotes the local binding of term1 to the variable ident in term2. There is a syntactic sugar for local definition of functions: let ident binder1 … bindern := term1 in term2 stands for
...

CURRENTLY STANDS
...
let ident := fun binder1 … bindern => term2 in term2.

BUT SHOULD PROBABLY BE:
...
let ident := fun binder1 … bindern => term1 in term2.

[coqbot]

Comment author: @letouzey

Thanks for spotting this. Fixed now in the svn archive...

Pierre Letouzey