Modify Init/Logic.v to compile with -mangle-names.

This is related to coq/coq#6781.

Most issues are with `destruct H` where H is the name of a binder
in the goal; this is addressed by moving dependent assumptions
before the colon. A different option would be adding `intros`
tactics, but this repeats the names of hypotheses (in the type of
the goal and in the proof script).

Additionally, the `destruct H with (Q:=...)` form gets changed to
`destruct (H ...)`, since the binder name `Q` is refreshed.

0 files changed, 0 insertions, 0 deletions