Make two or three definitions slightly smoother using the new make_reflection' constructor

Author: arnoudvanderleer

Modules/Signatures/EpiSigRepresentability.v

@@ -680,13 +680,12 @@ Proof.
   set (cond_F := fun R R_epi => inl ((Fepi R R_epi),, aepi) : cond_isEpi_hab R R_epi).
   apply left_adjoint_weq_reflections.
   intro R.
-  use make_reflection.
-  - use make_reflection_data.
-    + use (rep_of_b_in_R' R _ _ (cond_F R _ )).
-      * apply epiall.
-      * apply ii1.
-        apply epiall.
-    + apply projR_rep.
+  use make_reflection'.
+  - use (rep_of_b_in_R' R _ _ (cond_F R _ )).
+    + apply epiall.
+    + apply ii1.
+      apply epiall.
+  - apply projR_rep.
   - apply u_rep_universal.
 Qed.
 

Modules/SoftEquations/AdjunctionEquationRep.v

@@ -138,10 +138,10 @@ Section QuotientRep.
              (SigR_epis : ∏ (R : model Sig) , preserves_Epi (Sig R))
     : is_right_adjoint (ModEq_Mod_functor eq)
     := invmap (left_adjoint_weq_reflections _)
-      (λ (R : REP_CAT), make_reflection
-        (make_reflection_data (F := ModEq_Mod_functor eq)
-          (R' (modepis R) (SigR_epis R))
-          (projR_rep R (modepis R)(SigR_epis R )))
+      (λ (R : REP_CAT), make_reflection'
+        (F := ModEq_Mod_functor eq)
+        (R' (modepis R) (SigR_epis R))
+        (projR_rep R (modepis R)(SigR_epis R ))
         (u_rep_universal R (modepis R) (SigR_epis R))).