Fix some RepFor instances

Remove unused parameters, add Rep for empty type.

Author: pgiarrusso-sl

rocq-brick-libstdcpp/proof/mutex/spec/defer_lock_t.v

@@ -12,9 +12,8 @@ Section with_cpp.
     Import rep.RepFor.
     Import RepScheme.
 
-    (* <<std::defer_lock_t>> is a marker type, but it is empty, so ownership is not really
-       needed. *)
-    #[global] Instance repfor `{Σ : cpp_logic} : rep.RepFor.C "std::defer_lock_t" [] emp := {}.
+    #[global] Instance repfor `{Σ : cpp_logic} {σ : genv} :
+      rep.RepFor.C "std::defer_lock_t" [ArgType.CFrac] R := {}.
   End with_RepFor.
 
   cpp.spec "std::defer_lock_t::defer_lock_t(const std::defer_lock_t&)" as defer_lock_copy_ctor_spec from source with (

rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v

@@ -52,9 +52,8 @@ NES.Begin unique_lock.
     Import rep.RepFor.
     Import RepScheme.
 
-    #[global] Instance repfor `{Σ : cpp_logic} {σ : genv} ty {T} mutexR `{!BasicLockable ty (T:=T) mutexR}
-      (q : cQp.t) (om : option (M T)) :
-      rep.RepFor.C (Tnamed $ "std::unique_lock" .<< Atype ty >>) [ArgType.CFrac;ArgType.Constant _]
+    #[global] Instance repfor `{Σ : cpp_logic} {σ : genv} ty {T} mutexR `{!BasicLockable ty (T:=T) mutexR} :
+      rep.RepFor.C (Tnamed $ "std::unique_lock" .<< Atype ty >>) [ArgType.CFrac; ArgType.Constant _]
         (R ty mutexR) := {}.
   End with_RepFor.