Commit 0bde28f7 authored by Ralf Jung's avatar Ralf Jung
Browse files

Revert "turn canonical structures that don't have any instances into plain records"

This reverts commit 7266d16b
parent 7266d16b
Pipeline #84 passed with stage
...@@ -2,7 +2,7 @@ From algebra Require Export cmra. ...@@ -2,7 +2,7 @@ From algebra Require Export cmra.
(** * Functors from COFE to CMRA *) (** * Functors from COFE to CMRA *)
(* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *) (* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *)
Record iFunctor := IFunctor { Structure iFunctor := IFunctor {
ifunctor_car :> cofeT cmraT; ifunctor_car :> cofeT cmraT;
ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B; ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B); ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
......
...@@ -7,7 +7,7 @@ Local Arguments unit _ _ !_ /. ...@@ -7,7 +7,7 @@ Local Arguments unit _ _ !_ /.
(** * Definition of STSs *) (** * Definition of STSs *)
Module sts. Module sts.
Record stsT := STS { Structure stsT := STS {
state : Type; state : Type;
token : Type; token : Type;
prim_step : relation state; prim_step : relation state;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment