diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-24 15:50:17 +0000 |
| commit | ad0c122b1665fedde52f51ecdebb9d04a12831a6 (patch) | |
| tree | f19253819ee220024a38aa4509f01fe84adc4107 /theories/ZArith/ZArith.v | |
| parent | 7e00447c512b71543cec6b6fd63ec44106dada3d (diff) | |
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
Diffstat (limited to 'theories/ZArith/ZArith.v')
| -rw-r--r-- | theories/ZArith/ZArith.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index e532e4ad9..a935c7dac 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -13,7 +13,7 @@ Require Export ZArith_base. (** Extra definitions *) Require Export - Zpow_def Zsqrt_def Zlog_def Zgcd_def Zdiv_def Zdigits_def. + Zpow_def Zsqrt_def Zlog_def Zdiv_def Zdigits_def. (** Extra modules using [Omega] or [Ring]. *) |