diff options
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 88958d014..83f346242 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -304,10 +304,10 @@ let coq_le = lazy (init_constant "le") let coq_lt = lazy (init_constant "lt") let coq_ge = lazy (init_constant "ge") let coq_gt = lazy (init_constant "gt") -let coq_minus = lazy (init_constant "minus") -let coq_plus = lazy (init_constant "plus") -let coq_mult = lazy (init_constant "mult") -let coq_pred = lazy (init_constant "pred") +let coq_minus = lazy (init_constant "Nat.sub") +let coq_plus = lazy (init_constant "Nat.add") +let coq_mult = lazy (init_constant "Nat.mul") +let coq_pred = lazy (init_constant "Nat.pred") let coq_nat = lazy (init_constant "nat") let coq_S = lazy (init_constant "S") let coq_O = lazy (init_constant "O") |