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

This reverts commit 7266d16b76d170c70529c76920e046a08b5bdcc2
---
 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 90d9d708f..ecbd64bf1 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. *)
-Record iFunctor := IFunctor {
+Structure 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 915b372c7..4c2b1fb7b 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -7,7 +7,7 @@ Local Arguments unit _ _ !_ /.
 
 (** * Definition of STSs *)
 Module sts.
-Record stsT := STS {
+Structure stsT := STS {
   state : Type;
   token : Type;
   prim_step : relation state;
-- 
GitLab