1. Where CompCert uses list_repeat,zlt,zeq that have since been
  added to the Coq Standard Library as repeat, Z_lt_ge_dec, Z.eq_dec,
  use the Standard Library versions instead of the CompCert versions.

2. Make the list_solver (floyd/sublist, floyd/Znth_solve, floyd/list_solver)
  mostly independent of CompCert and VST, so that it can be used
  in other developments besides VST.