Fix non-forgetful inheritance

math-comp · Dec 25, 2020 · e954498 · e954498
1 parent 733b758
commit e954498
Show file tree

Hide file tree

Showing 5 changed files with 1,025 additions and 600 deletions.
diff --git a/theories/derive.v b/theories/derive.v
@@ -25,6 +25,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
+Import nonforgetful_inheritance.Exports.
 
 Local Open Scope ring_scope.
 Local Open Scope classical_set_scope.

diff --git a/theories/ereal.v b/theories/ereal.v
@@ -58,6 +58,7 @@ Unset Printing Implicit Defensive.
 Declare Scope ereal_scope.
 
 Import Order.TTheory GRing.Theory Num.Theory.
+Import nonforgetful_inheritance.Exports.
 
 Local Open Scope ring_scope.
 
@@ -211,10 +212,10 @@ Notation "x < y <= z"  := ((lte x y) && (lee y z)) : ereal_scope.
 Notation "x <= y < z"  := ((lee x y) && (lte y z)) : ereal_scope.
 Notation "x < y < z"   := ((lte x y) && (lte y z)) : ereal_scope.
 
-Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E) = (x <= y)%O.
+Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E) = (x <= y)%R.
 Proof. by []. Qed.
 
-Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E) = (x < y)%O.
+Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E) = (x < y)%R.
 Proof. by []. Qed.
 
 Lemma lte_pinfty (R : realDomainType) (x : R) : x%:E < +oo.
@@ -627,10 +628,10 @@ Lemma le0R (x : {ereal R}) :
   0%:E <= x -> (0 <= real_of_er(*TODO: coercion broken*) x)%R.
 Proof. by case: x. Qed.
 
-Lemma lee_tofin (r0 r1 : R) : (r0 <= r1)%O -> r0%:E <= r1%:E.
+Lemma lee_tofin (r0 r1 : R) : (r0 <= r1)%R -> r0%:E <= r1%:E.
 Proof. by []. Qed.
 
-Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%O -> r0%:E < r1%:E.
+Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%R -> r0%:E < r1%:E.
 Proof. by []. Qed.
 
 End ERealOrderTheory.