Commit 7266d16b authored by Ralf Jung's avatar Ralf Jung
Browse files

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

parent d350e4f6
...@@ -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. *)
Structure iFunctor := IFunctor { Record 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.
Structure stsT := STS { Record 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