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).