Big cleanup

[sonmarcho]

This is the companion PR of AeneasVerif/charon#50.
In addition to propagating changes coming from Charon and using the new functionalities provided by Charon (for instance, the name matchers to map external definitions to definitions in the standard library, and the computation of the regions hierarchy) we performed the following modifications:

• cleaned up the "Extract" files, to remove the formatter type, which proved not useful anymore and quite cumbersome.
• add code spans in the comments of the generated code
• use typing information to generate names for the trait clauses and the trait parent clauses. For instance, if a function requires a trait clause for Trait<T, u32>, we now generate a name like TraitTU32Inst, instead of inst followed by the index of the clause.