Updating Coq files to fix the Inductive optional sort (it was mandatory before).