unification hint nat ≔ [ id [ : term ] ,.. ] ; [ id ≟ term ,.. ] ⊢ term ≡ term

Declares the hint at precedence n

The file hints_declaration.ma must be included to declare hints with that syntax.

Unification hints are described in the paper "Hints in unification" by Asperti, Ricciotti, Sacerdoti and Tassi.