Fixing bugs in doc about when "with" is needed or not to give bindings to tactics.
Fixing bugs in doc about when "with" is needed or not to give bindings
to tactics.

git-svn-id: 44dc50bdcc0f5d1a212c497508dc9452e0b35e2b@14761 85f007b7-540e-0410-9357-904b9bb8a0f7

maximedenes/native-coq,maximedenes/native-coq,maximedenes/native-coq