diff options
| author | filliatr | 2001-04-10 14:45:40 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-10 14:45:40 +0000 |
| commit | 7fe97cf3e53fe94c6a6bdd2a0a5c869d9bf7092e (patch) | |
| tree | 38a7b285997d76d1799b397f3fa443e4713a4627 /contrib/omega | |
| parent | 45d82e91c30f912740211060b4cdb7cb83226157 (diff) | |
portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1573 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 15022750a3..16bbd614f1 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -228,6 +228,7 @@ let constant dir s = anomaly ("Coq_omega: cannot find "^ (Nametab.string_of_qualid (Nametab.make_qualid dir id))) +let arith_constant dir = constant ("Arith"::dir) let zarith_constant dir = constant ("Zarith"::dir) let logic_constant dir = constant ("Logic"::dir) @@ -266,7 +267,7 @@ let coq_inj_ge = lazy (zarith_constant ["auxiliary"] "inj_ge") let coq_inj_gt = lazy (zarith_constant ["auxiliary"] "inj_gt") let coq_inj_neq = lazy (zarith_constant ["auxiliary"] "inj_neq") let coq_inj_eq = lazy (zarith_constant ["auxiliary"] "inj_eq") -let coq_pred_of_minus = lazy (zarith_constant ["auxiliary"] "pred_of_minus") +let coq_pred_of_minus = lazy (arith_constant ["Minus"] "pred_of_minus") let coq_fast_Zplus_assoc_r = lazy (zarith_constant ["auxiliary"] "fast_Zplus_assoc_r") let coq_fast_Zplus_assoc_l = lazy (zarith_constant ["auxiliary"] "fast_Zplus_assoc_l") let coq_fast_Zmult_assoc_r = lazy (zarith_constant ["auxiliary"] "fast_Zmult_assoc_r") |