Merge pull request #105 from math-comp/fix_87

CohenCyril · web-flow · commit 5d48590bf02d · 2020-08-07T23:13:45.000+02:00
removing spurious empty TYPE structure
diff --git a/demo1/hierarchy_0.v b/demo1/hierarchy_0.v
@@ -5,8 +5,6 @@ From HB Require Import structures.
 (* Stage 0: +Ring+                                                        *)
 (**************************************************************************)
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record Ring_of_TYPE A := {
   zero : A;
   one : A;
diff --git a/demo1/hierarchy_1.v b/demo1/hierarchy_1.v
@@ -5,8 +5,6 @@ From HB Require Import structures.
 (* Stage 1: +AddComoid+ -> Ring                                           *)
 (**************************************************************************)
 
-HB.structure Definition TYPE := { A of True }.
-
 (* Begin change *)
 
 HB.mixin Record AddComoid_of_TYPE A := {
diff --git a/demo1/hierarchy_2.v b/demo1/hierarchy_2.v
@@ -5,8 +5,6 @@ From HB Require Import structures.
 (* Stage 2: AddComoid -> +AddAG+ -> Ring                                  *)
 (**************************************************************************)
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddComoid_of_TYPE A := {
   zero : A;
   add : A -> A -> A;
diff --git a/demo1/hierarchy_3.v b/demo1/hierarchy_3.v
@@ -7,8 +7,6 @@ From HB Require Import structures.
 (*                     -> +SemiRing+ -                                    *)
 (**************************************************************************)
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddComoid_of_TYPE A := {
   zero : A;
   add : A -> A -> A;
diff --git a/demo1/hierarchy_4.v b/demo1/hierarchy_4.v
@@ -7,8 +7,6 @@ From HB Require Import structures.
 (*                                    -> SemiRing -                       *)
 (**************************************************************************)
 
-HB.structure Definition TYPE := { A of True }.
-
 (* Begin change *)
 HB.mixin Record AddMonoid_of_TYPE S := {
   zero : S;
diff --git a/demo1/hierarchy_5.v b/demo1/hierarchy_5.v
@@ -7,8 +7,6 @@ From HB Require Import structures.
 (*                      -> +BiNearRing+ -> SemiRing -                     *)
 (**************************************************************************)
 
-HB.structure Definition TYPE := { A of True }.
-
 HB.mixin Record AddMonoid_of_TYPE S := {
   zero : S;
   add : S -> S -> S;
