diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 14:44:08 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 14:44:08 +0000 |
| commit | df7acfad0ce0270b62644a5e9f8709ed0e7936e6 (patch) | |
| tree | 746850496c47f6618219ad5d5560f021b7b8e56b /plugins/nsatz | |
| parent | e5c4bc888c1f0516928a32f70529f95e36243c5d (diff) | |
Move stuff about positive into a distinct PArith subdir
Beware! after this, a ./configure must be done. It might also
be a good idea to chase any phantom .vo remaining after a make clean
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/nsatz.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 5070f89ed..b235b5821 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -189,9 +189,9 @@ let z0 = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z0") let zpos = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Zpos") let zneg = lazy(gen_constant "CC" ["ZArith";"BinInt"] "Zneg") -let pxI = lazy(gen_constant "CC" ["NArith";"BinPos"] "xI") -let pxO = lazy(gen_constant "CC" ["NArith";"BinPos"] "xO") -let pxH = lazy(gen_constant "CC" ["NArith";"BinPos"] "xH") +let pxI = lazy(gen_constant "CC" ["PArith";"BinPos"] "xI") +let pxO = lazy(gen_constant "CC" ["PArith";"BinPos"] "xO") +let pxH = lazy(gen_constant "CC" ["PArith";"BinPos"] "xH") let nN0 = lazy (gen_constant "CC" ["NArith";"BinNat"] "N0") let nNpos = lazy(gen_constant "CC" ["NArith";"BinNat"] "Npos") |