From b4d93b850308751b1b0587ca92d633d6df4db7bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Thu, 19 Sep 2024 13:46:40 +0200
Subject: [PATCH] `Admitted` does not emit univ constraints from the proof

Fix #19566 (introduced in 3b4cf49e39ccb506aeb317aab818dc2fdc828175)
---
 test-suite/bugs/bug_18951.v |  3 ++-
 test-suite/bugs/bug_19566.v |  7 +++++++
 vernac/declare.ml           | 13 ++++---------
 3 files changed, 13 insertions(+), 10 deletions(-)
 create mode 100644 test-suite/bugs/bug_19566.v

diff --git a/test-suite/bugs/bug_18951.v b/test-suite/bugs/bug_18951.v
index 108b38a58b68..96de82154d4e 100644
--- a/test-suite/bugs/bug_18951.v
+++ b/test-suite/bugs/bug_18951.v
@@ -10,4 +10,5 @@ Proof.
 Fail Admitted. (* Has still evars *)
 Unshelve.
 3:exact nat.
-Admitted.
+Fail Admitted.
+Abort.
diff --git a/test-suite/bugs/bug_19566.v b/test-suite/bugs/bug_19566.v
new file mode 100644
index 000000000000..e380b7c4a287
--- /dev/null
+++ b/test-suite/bugs/bug_19566.v
@@ -0,0 +1,7 @@
+
+Universes u v.
+Lemma foo : Type@{v}.
+  exact Type@{u}.
+Admitted.
+
+Check Type@{v} : Type@{u}.
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 72004ca3f368..50ee024a8f75 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -2246,7 +2246,7 @@ let check_type_evars_solved env sigma typ =
   let evars = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma typ) in
   match evars with
   | [] -> ()
-  | evk::_ -> CErrors.user_err (str "Cannot admit: the statement has still unresolved existential variables.")
+  | evk::_ -> CErrors.user_err (str "Cannot admit: the statement has unresolved existential variables.")
 
 let finish_admitted ~pm ~pinfo ~uctx ~sec_vars typs =
   (* If the constant was an obligation we need to update the program map *)
@@ -2261,17 +2261,12 @@ let finish_admitted ~pm ~pinfo ~uctx ~sec_vars typs =
     pm
 
 let save_admitted ~pm ~proof =
-  let Proof.{ entry; sigma } = Proof.data (get proof) in
-  let typs = List.map pi3 (Proofview.initial_goals entry) in
-  List.iter (check_type_evars_solved (Global.env()) sigma) typs;
   let iproof = get proof in
+  let Proof.{ entry } = Proof.data iproof in
+  let typs = List.map pi3 (Proofview.initial_goals entry) in
+  let sigma = Evd.from_ctx proof.initial_euctx in
   List.iter (check_type_evars_solved (Global.env()) sigma) typs;
   let sec_vars = compute_proof_using_for_admitted proof.pinfo proof typs iproof in
-  (* We have the choice of taking CInfo.typ and initial_euctx or or
-     the typs and uctx from the type. By uniformity we would like to
-     do the same as in save_lemma_admitted_delayed, but we would need
-     for that that fixpoints are represented with multi-statements; so
-     we take the initial types *)
   let sigma = Evd.minimize_universes sigma in
   let typs = List.map (EConstr.to_constr sigma) typs in
   let uctx = Evd.ustate sigma in