The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Cedric,

 

yes, instantiating the evar explicitly would destroy the proof automation. Except for this issue, a single eauto with HDBhoare would do it for the complete goal (the H_Consequence_pre is in the hint database). But since I now understood the problem with your help, maybe I can find a solution.

 

Best regards,

 

Michael