Improved ltac code for zify (fix #2575).
Improved ltac code for zify (fix #2575).

 Note nonetheless that the underlying bug is still active (cf. #2602),
 I've just written the ltac stuff in a nicer way (no nested match goal),
 and things happen to work now :-)

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

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