From 7266d16b76d170c70529c76920e046a08b5bdcc2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 09:08:53 +0100
Subject: [PATCH] turn canonical structures that don't have any instances into
 plain records

---
 algebra/functor.v | 2 +-
 algebra/sts.v     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/algebra/functor.v b/algebra/functor.v
index ecbd64bf1..90d9d708f 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 4c2b1fb7b..915b372c7 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;
-- 
GitLab