diff options
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/ZMicromega.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 6d0f40ac13..2db4db6765 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -1009,12 +1009,7 @@ Definition eval := eval_formula. Definition prod_pos_nat := prod positive nat. -Definition n_of_Z (z:Z) : N := - match z with - | Z0 => N0 - | Zpos p => Npos p - | Zneg p => N0 - end. +Notation n_of_Z := Z.to_N (only parsing). (* Local Variables: *) (* coding: utf-8 *) |