From bcac37c59625189a7013572480ccdb719518604d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 May 2019 12:29:50 +0200
Subject: [PATCH] Make functors a `Record` instead of a `Structure`.

We never make canonical instances of them.
---
 theories/algebra/cmra.v | 4 ++--
 theories/algebra/ofe.v  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 7059e8b61..ed6254f0b 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -765,7 +765,7 @@ Section cmra_morphism.
 End cmra_morphism.
 
 (** Functors *)
-Structure rFunctor := RFunctor {
+Record rFunctor := RFunctor {
   rFunctor_car : ofeT → ofeT → cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
@@ -798,7 +798,7 @@ Coercion constRF : cmraT >-> rFunctor.
 Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
 
-Structure urFunctor := URFunctor {
+Record urFunctor := URFunctor {
   urFunctor_car : ofeT → ofeT → ucmraT;
   urFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index f7672c263..6db8d6e80 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -663,7 +663,7 @@ Instance prodC_map_ne {A A' B B'} :
 Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
 (** Functors *)
-Structure cFunctor := CFunctor {
+Record cFunctor := CFunctor {
   cFunctor_car : ofeT → ofeT → ofeT;
   cFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
-- 
GitLab