fix tactic ehoare-if

[bgregoir]

No description provided.

[fdupress]

Why is this change necessary and how should one approach modifying proofs?

[loutr]

Why is this change necessary and how should one approach modifying proofs?

This is a fix for the if tactic in the ehoare logic that solves an anomaly I encountered when updating a proof and discussed with Benjamin. The underlying rcond tactic for phoare and ehoare logic were behaving the same, assuming that the precondition is a (newly-formed) conjunction, which is syntactically inconsistent (as ehoare preconditions are (functions to the) reals). Supposedly all instances of the if tactic in a ehoare goal had the same anomaly in the latest eC version.

The "new" behaviour is the expected one and there should be little to no modifications required.