diff options
| author | letouzey | 2008-04-16 23:51:06 +0000 |
|---|---|---|
| committer | letouzey | 2008-04-16 23:51:06 +0000 |
| commit | 286d7e8201de98dc5cc36b6fbda8f9c1126f37ea (patch) | |
| tree | 1ec5317554f488d8abd722e66a7d341d6cf521f1 /kernel/cbytecodes.ml | |
| parent | 99ad573113f5afc8bb5409649843567dee40ba40 (diff) | |
Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)
This way, no more references to NBinDefs.N when doing "Print N".
Long-term migration to theories/Numbers is still planned, but it needs
more works, for instance to adapt both positive and N and Z at once.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions