diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 13:07:42 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 13:07:42 +0000 |
| commit | cb9061d894d516e4607a9237813402d929384b26 (patch) | |
| tree | 13137c2d2587c29483dbee0035ae1eab20f6342b /contrib/omega/coq_omega.ml | |
| parent | 97271bd7c99f2a6de4b022af420f7a6050803492 (diff) | |
remplace Zarith par ZArith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1625 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega/coq_omega.ml')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 16bbd614f..e17336a71 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -229,7 +229,7 @@ let constant dir s = (Nametab.string_of_qualid (Nametab.make_qualid dir id))) let arith_constant dir = constant ("Arith"::dir) -let zarith_constant dir = constant ("Zarith"::dir) +let zarith_constant dir = constant ("ZArith"::dir) let logic_constant dir = constant ("Logic"::dir) (* fast_integer *) @@ -398,12 +398,12 @@ let make_coq_path dir s = (Nametab.string_of_qualid (Nametab.make_qualid dir id))^ " is not a constant") -let sp_Zs = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zs") -let sp_Zminus = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zminus") -let sp_Zle = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zle") -let sp_Zgt = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zgt") -let sp_Zge = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zge") -let sp_Zlt = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zlt") +let sp_Zs = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zs") +let sp_Zminus = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zminus") +let sp_Zle = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zle") +let sp_Zgt = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zgt") +let sp_Zge = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zge") +let sp_Zlt = lazy (make_coq_path ["ZArith";"zarith_aux"] "Zlt") let sp_not = lazy (make_coq_path ["Init";"Logic"] "not") let mk_var v = mkVar (id_of_string v) |