From 44e8df83ad4e4394a96c15c787405cdea8931074 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Wed, 30 Oct 2019 14:40:23 +0100
Subject: Rename: (l|L)attice -> (d|D)istrLattice

---
 mathcomp/field/algebraics_fundamentals.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 4fe5f70..4824697 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -589,7 +589,8 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
   pose QyNum : realLtMixin (Q y) :=
     RealLtMixin posD posM posNneg posB posVneg absN absE (rrefl _).
   pose QyOrder :=
-    OrderType (LatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum.
+    OrderType
+      (DistrLatticeType (POrderType ring_display (Q y) QyNum) QyNum) QyNum.
   pose QyNumField := [numFieldType of NumDomainType QyOrder QyNum].
   pose Ry := [realFieldType of [realDomainType of QyNumField]].
   have archiRy := @rat_algebraic_archimedean Ry _ alg_integral.
-- 
cgit v1.2.3