diff --git a/modures/cmra.v b/modures/cmra.v
index bce7993314f8ae07beb4fe4b98632cb3e1fbbcda..b9e50b52804744ecc7635b7f5ba9fa14f96970fb 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -296,6 +296,9 @@ Section discrete.
 End discrete.
 Arguments discreteRA _ {_ _ _ _ _ _}.
 
+(** CMRA for the unit type *)
+Canonical Structure unitRA : cmraT := discreteRA ().
+
 (** Product *)
 Section prod.
   Context {A B : cmraT}.
diff --git a/modures/ra.v b/modures/ra.v
index a3c5d4e0ba4531476a875a9526bc743fc66fe859..bfc324de4ece896dcd375cc1e8c7b4193c9a0b88 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -231,3 +231,21 @@ Ltac solve_included :=
   ra_reflection.quote;
   apply ra_reflection.flatten_correct, (bool_decide_unpack _);
   vm_compute; apply I.
+
+(** An RA for the unit type *)
+Instance unit_valid : Valid () := λ x, True.
+Instance unit_unit : Unit () := λ x, x.
+Instance unit_op : Op () := λ x y, tt.
+Instance unit_minus : Minus () := λ x y, tt.
+
+Instance unit_ra : RA ().
+Proof.
+  split; done.
+Qed.
+
+
+Instance unit_empty : Empty () := tt.
+Instance unit_empty_ra : RAIdentity().
+Proof.
+  split; done.
+Qed.