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/vo.itarget | |
| 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/vo.itarget')
| -rw-r--r-- | theories/ZArith/vo.itarget | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget index cf0cdd7c7..7592d2fae 100644 --- a/theories/ZArith/vo.itarget +++ b/theories/ZArith/vo.itarget @@ -32,6 +32,5 @@ Zsqrt_compat.vo Zwf.vo Zsqrt_def.vo Zlog_def.vo -Zgcd_def.vo Zeuclid.vo Zdigits_def.vo
\ No newline at end of file |