What means (a:b) c and [a:b] c in some Coq theories and where is it defined?

I have seen a very strange syntax:开发者_开发问答 (name:type1) type2 in type and [name:type] expr in expressions, looks like alternate syntax for Pi and Lambda, but I haven't found anything in documentation after several hours of searching, all in vain.

What is it means and where it is defined? (Sorry I've lost link to example usage)

---

You've been reading a theory written for an older version of Coq. The syntax got a major rehaul with V8.0. V8.0 shipped with a tool to translate V7 theories into V8, which worked pretty well; the tool was dropped from subsequent releases.

You can see a review of changes in the paper Translation from Coq V7 to V8.

In particular, (a:b) c is a universal quantification, now written forall a:b, c; [a:b] c is a lambda abstraction, now written fun a:b => c. Another important thing when reading old theories is that function application required parentheses and had low precedence: up to V7, (f x = y) meant (f (x=y)) and ([x:nat]y z) meant (([x:nat]y) z).