'Curly brace proof syntax: begin x. = { auto } y. []

I've seen the following syntax used in Coq proofs, with variations to the relation (=) and the tactic (auto):

begin
  x.
= { auto }
  y.
= { auto }
  z.
[].

What's the name of this syntactic construct, and where is it documented?

coq

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Solution	Source