Close coq#18636 and add some code comments

Fixed by reverting fea5fcc

The reason the first abstract changes the behaviour is that it changes which branch we take in https://github.com/coq/coq/blob/3d86c1d4569b0a25a00677833b9f47c3059a8345/vernac/declare.ml#L1826

Why we have this code is not clear but removing it (so it becomes just `if not poly && keep_body_ucst_separate`) causes undefined universe anomaly at https://github.com/coq/coq/blob/3d86c1d4569b0a25a00677833b9f47c3059a8345/test-suite/success/rewrite.v#L50

In any case with this code and fea5fcc (indeed from coq#17745) we use an unminimized initial_euctx which has `{foo.5} |= Set = foo.5` which is added to the global env (we are in univ monomorphic mode), and since monomorphic universes are declared `> Set` we get the error.

I guess short term we should revert fea5fcc and long term we should look into not checking is_empty_private_constants.

(cherry picked from commit 14685d5)

doc/changelog/04-tactics/18640-fix-double-abstract.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  undeclared universe with multiple uses of :tacn:`abstract`
+  (`#18640 <https://github.com/coq/coq/pull/18640>`_,
+  fixes `#18636 <https://github.com/coq/coq/issues/18636>`_,
+  by Gaëtan Gilbert).

test-suite/bugs/bug_18636.v

@@ -0,0 +1,9 @@
+Polymorphic Axiom array@{u} : Type@{u} -> Type@{u}.
+Polymorphic Axiom get : forall {A} (t : array A), A.
+
+Lemma foo (t: array nat): True.
+Proof.
+assert True by abstract exact I.
+assert (v := get t).
+abstract exact I. (* Universe inconsistency. Cannot enforce Top.5 = Set because Set < Top.5. *)
+Qed.

vernac/declare.ml

@@ -1823,6 +1823,9 @@ let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate ps =
       (* allow_deferred case *)
       if not poly &&
          (keep_body_ucst_separate
+          (* checking is_empty_private_constants prevents an undefined universe anomaly
+             cf test-suite/success/rewrite.v Qed for lemma l1
+             not sure what's going on, there's probably a better way to work *)
           || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
       then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl t b
       (* private_poly_univs case *)
@@ -1930,7 +1933,9 @@ let build_by_tactic env ~uctx ~poly ~typ tac =
 let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
   let sigma, concl =
     (* FIXME: should be done only if the tactic succeeds *)
-    (* XXX maybe we can fix now that we support evars *)
+    (* XXX maybe we can fix now that we support evars
+       if close_proof stops caring about is_empty_private_constants we can remove the minimization
+       see #18636 *)
     let sigma = Evd.minimize_universes sigma in
     sigma, Evarutil.nf_evar sigma concl
   in