diff options
Diffstat (limited to 'mathcomp/algebra/rat.v')
| -rw-r--r-- | mathcomp/algebra/rat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 4ef050f..8478d93 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -19,7 +19,7 @@ From mathcomp Require Import ssrint. (* ratr x == generic embedding of (r : R) into an arbitrary unitring. *) (******************************************************************************) -Import Order.Theory GRing.Theory Num.Theory. +Import Order.TTheory GRing.Theory Num.Theory. Set Implicit Arguments. Unset Strict Implicit. |