Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
removing spurious empty TYPE structure
fixes #87
  • Loading branch information
CohenCyril committed Aug 7, 2020
1 parent 27ff0c0 commit f9372c6
Show file tree
Hide file tree
Showing 6 changed files with 0 additions and 12 deletions.
2 changes: 0 additions & 2 deletions demo1/hierarchy_0.v
Expand Up @@ -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;
Expand Down
2 changes: 0 additions & 2 deletions demo1/hierarchy_1.v
Expand Up @@ -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 := {
Expand Down
2 changes: 0 additions & 2 deletions demo1/hierarchy_2.v
Expand Up @@ -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;
Expand Down
2 changes: 0 additions & 2 deletions demo1/hierarchy_3.v
Expand Up @@ -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;
Expand Down
2 changes: 0 additions & 2 deletions demo1/hierarchy_4.v
Expand Up @@ -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;
Expand Down
2 changes: 0 additions & 2 deletions demo1/hierarchy_5.v
Expand Up @@ -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;
Expand Down

0 comments on commit f9372c6

Please sign in to comment.