Fix [rewrite@A]

When the hypothesis contained [a @ (b @ c)] where the implicit arguments
to [concat] did not match the implicit arguments inferred for [@concat _
_ _ _ a (@concat _ _ _ _ b c)] (according to [pattern]),
[left_associate_concat_in] looped, repeatedly finding [a @ (b @ c)], and
failing to associate it to the left, introducing constant transports
that did nothing.

This is now fixed, by picking up and passing the implicit arguments,
explicitly.

The comment in Modalities/ReflectiveSubuniverse.v has been updated; a
naive use of [rewrite@A] causes the subsequent rewrite to fail.  I
haven't tracked it down, but I suspect @mikeshulman wouldn't have much
trouble updating the file.

This fixes #744; the test is now added to Tests.v.

theories/Modalities/ReflectiveSubuniverse.v

@@ -921,7 +921,7 @@ Section Reflective_Subuniverse.
           rewrite concat_pp_p in p.
           apply moveR_Vp in p.
           rewrite@A <- p; clear p.
-          (** for the next one, [rewrite@A] spins forever *)
+          (** TODO: use [rewrite@A] here *)
           apply moveL_pV; rewrite !concat_pp_p; apply moveR_Vp.
           rewrite (to_O_natural_compose g
                        (fun x => @coeq _ _ (O_functor f) (O_functor g)

theories/Tactics/RewriteModuloAssociativity.v

@@ -195,8 +195,8 @@ Module Export Concat.
                                 let T' := (eval cbv beta zeta in T) in
                                 let ret' := (eval cbv beta zeta in ret) in
                                 constr:(ret' : T')
-      | context[?a @ (?b @?c)] =>
-        (lazymatch eval pattern (a @ (b @ c)) in T with
+      | context[@concat ?A1 ?x1 ?y1 ?z1 ?a (@concat ?A2 ?x2 ?y2 ?z2 ?b ?c)] =>
+        (lazymatch eval pattern (@concat A1 x1 y1 z1 a (@concat A2 x2 y2 z2 b c)) in T with
         | ?P _ => let H' := constr:(transport P (concat_p_pp a b c) H) in
                   rec_tac H'
          end)

theories/Tests.v

@@ -23,3 +23,14 @@ Check (@ispointed_susp Set).
 
 (** Check that nested sigma-type notation didn't get clobbered by surreal cuts *)
 Check ({ l : Unit & { n : Unit & Unit }}).
+
+(** Regression check issue #744 *)
+Module Foo (Os : ReflectiveSubuniverses).
+  Module Import Os_Theory := ReflectiveSubuniverses_Theory Os.
+  Goal Unit.
+    let lem' := preconcat_any @to_O_natural_compose in
+    pose proof lem' as H.
+    let test := left_associate_concat_in H in
+    pose test.
+  Admitted.
+End Foo.