diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 9e3674a23d..49a60916aa 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -17,7 +17,7 @@ Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite spec_0 spec_succ spec_add spec_mul spec_pred spec_sub spec_div spec_modulo spec_gcd spec_compare spec_eq_bool - spec_max spec_min + spec_max spec_min spec_power_pos spec_power : nsimpl. Ltac nsimpl := autorewrite with nsimpl. Ltac ncongruence := unfold eq; repeat red; intros; nsimpl; congruence. @@ -252,5 +252,5 @@ Qed. End NTypeIsNAxioms. Module NType_NAxioms (N : NType) - <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N + <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N <: HasMinMax N := N <+ NTypeIsNAxioms. |