CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defined names in term binders.

Closes #3747.
EqdepFacts: generalize statements which were wrongly restricted to Prop.
Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].
Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of future goals).

Fixes #3757. Thanks to Hugo for helping pinpoint the issue.
Refine tactic: simplify the conclusion only at the end of the tactic.

It was the intended semantics from the beginning. I just wrote it wrong.

Spotted by Hugo, fix by Hugo.