Grazie!
Il nome file, nel mio caso sarebbe $_FILES['user_file'] (oppure $file)?

Ho risolto scrivendo:
Codice PHP:
$controllo_file = pathinfo($file['name']);
echo 'Estensione: ' . $controllo_file['extension']; 
Allora non ho capito niente! Se patchinfo() vuole un array io gli davo $file e non va bene. Se metto $file[nome] allora va bene???
Ma $file[nome] è un campo dell'array, mentre $file E' l'array!
Non capisco...