diff options
| author | Kazuhiko Sakaguchi | 2019-12-03 23:11:03 +0900 |
|---|---|---|
| committer | Cyril Cohen | 2019-12-11 14:26:52 +0100 |
| commit | 3f6aa286677f6cb0659300afd2b612b7bce20e73 (patch) | |
| tree | 1a2abb3ee70e24b31ece51f6bc5b8a2ea248d6a2 /mathcomp/algebra | |
| parent | 0d7ffe8610da33bdce2cf7f612eef7e5a777cd8e (diff) | |
The compatibility module in ssrnum should now be for version 1.10
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 1f6c0a4..05ac8ed 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -26,7 +26,7 @@ From mathcomp Require Import ssralg poly. (* normedZmodType R *) (* == interface for a normed Zmodule structure indexed by *) (* numDomainType R. *) -(* NormedZmodType R T m *) +(* NormedZmodType R T m *) (* == pack the normed Zmodule mixin into a normedZmodType. *) (* The carrier T must have an integral domain structure. *) (* [normedZmodType R of T for S] *) @@ -5039,7 +5039,7 @@ Export Num.RealLeMixin.Exports Num.RealLtMixin.Exports. Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin. (* compatibility module *) -Module mc_1_9. +Module mc_1_10. Module Num. (* If you failed to process the next line in the PG or the CoqIDE, replace *) (* all the "ssrnum.Num" with "Top.Num" in this module to process them, and *) @@ -5617,4 +5617,4 @@ Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F] format "[ 'arg' 'maxr_' ( i > i0 ) F ]") : form_scope. End Num. -End mc_1_9. +End mc_1_10. |