diff --git a/algebra/functor.v b/algebra/functor.v
index ecbd64bf15f551f25b8a769032085883e3ced447..90d9d708f7c67c4dc251a2fd03d09eb86dc44598 100644
--- a/algebra/functor.v
+++ b/algebra/functor.v
@@ -2,7 +2,7 @@ From algebra Require Export cmra.
 
 (** * Functors from COFE to CMRA *)
 (* 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_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);
diff --git a/algebra/sts.v b/algebra/sts.v
index 4c2b1fb7b921cf1ce41afac527222aabd0697b47..915b372c746111f3b755b1890dd5f294cd497b24 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -7,7 +7,7 @@ Local Arguments unit _ _ !_ /.
 
 (** * Definition of STSs *)
 Module sts.
-Structure stsT := STS {
+Record stsT := STS {
   state : Type;
   token : Type;
   prim_step : relation state;