Clean-up of Znumtheory, deletion of Zgcd_def

 In particular, we merge the old Zdivide (used to be an ad-hoc
 inductive predicate) and the new Z.divide (based on exists).
 Notations allow to do that (almost) transparently, the only
 impact is that the name picked by the system will not be "q"
 anymore when destructing a Z.divide. Some fragile scripts
 may have to be fixed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14239 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions