diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-30 14:40:52 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-30 14:40:52 +0000 |
commit | bb46716e2fbbc85386429a429de284a6f521c57c (patch) | |
tree | 0f282fc671b988a0337f6a64f0c0230813c99717 /lib | |
parent | 962c2260406c630e90bb001bd9238dea72eef0c1 (diff) |
Cleanup in SpecViaZ
Note that in NSig (and hence NMake and BigN), to_N is now
Z.to_N (to_Z ...) instead of Z.abs_N (to_Z ...). This doesn't
change the result (since to_Z create non-negative integers),
but some proofs may have to be adapted
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14250 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions