Commit bcac37c5 authored by Robbert Krebbers's avatar Robbert Krebbers

Make functors a `Record` instead of a `Structure`.

We never make canonical instances of them.
parent 607933e0
......@@ -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;
......
......@@ -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;
......
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