Reimplement Admit Obligations using standard Admitted code

Fix #13109

2 files changed, 39 insertions, 23 deletions

diff --git a/test-suite/bugs/closed/bug_13109.v b/test-suite/bugs/closed/bug_13109.v
new file mode 100644
index 0000000000..76511a44c5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13109.v
@@ -0,0 +1,24 @@
+Require Import Coq.Program.Tactics.
+
+Set Universe Polymorphism.
+Obligation Tactic := idtac.
+
+Program Definition foo : Type := _.
+Program Definition bar : Type := _.
+Admit Obligations.
+(* Error: Anomaly "Uncaught exception AcyclicGraph.Make(Point).AlreadyDeclared."
+Please report at http://coq.inria.fr/bugs/.
+ *)
+Print foo.
+Print foo_obligation_1.
+Print bar.
+Print bar_obligation_1.
+
+Program Definition baz : Type := _.
+Admit Obligations of baz.
+Print baz.
+Print baz_obligation_1.
+
+Admit Obligations.
+
+Fail Admit Obligations of nobody.
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 099a63cf8f..ae7878b615 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -725,7 +725,6 @@ module Obligation = struct
     ; obl_tac : unit Proofview.tactic option }
 
   let set_type ~typ obl = {obl with obl_type = typ}
-  let set_body ~body obl = {obl with obl_body = Some body}
 end
 
 type obligations = {obls : Obligation.t array; remaining : int}
@@ -2464,32 +2463,25 @@ let add_mutual_definitions l ~pm ~info ?obl_hook ~uctx
   in
   pm
 
-let admit_prog ~pm prg =
-  let {obls; remaining} = Internal.get_obligations prg in
-  let obls = Array.copy obls in
-    Array.iteri
-      (fun i x ->
-        match x.obl_body with
-        | None ->
-            let x = subst_deps_obl obls x in
-            let uctx = Internal.get_uctx prg in
-            let univs = UState.univ_entry ~poly:false uctx in
-            let kn = declare_constant ~name:x.obl_name ~local:Locality.ImportNeedQualified
-              (ParameterEntry (None, (x.obl_type, univs), None)) ~kind:Decls.(IsAssumption Conjectural)
-            in
-              assumption_message x.obl_name;
-              obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x
-        | Some _ -> ())
-      obls;
-  Obls_.update_obls ~pm prg obls 0
-
-(* get_any_prog *)
+let rec admit_prog ~pm prg =
+  let {obls} = Internal.get_obligations prg in
+  let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
+  let i = match Array.findi is_open obls with
+    | Some i -> i
+    | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.")
+  in
+  let proof = solve_obligation prg i None in
+  let pm = Proof.save_admitted ~pm ~proof in
+  match ProgMap.find_opt (Internal.get_name prg) pm with
+  | Some prg -> admit_prog ~pm (CEphemeron.get prg)
+  | None -> pm
+
 let rec admit_all_obligations ~pm =
   let prg = State.first_pending pm in
   match prg with
   | None -> pm
   | Some prg ->
-    let pm, _prog = admit_prog ~pm prg in
+    let pm = admit_prog ~pm prg in
     admit_all_obligations ~pm
 
 let admit_obligations ~pm n =
@@ -2497,7 +2489,7 @@ let admit_obligations ~pm n =
   | None -> admit_all_obligations ~pm
   | Some _ ->
     let prg = get_unique_prog ~pm n in
-    let pm, _ = admit_prog ~pm prg in
+    let pm = admit_prog ~pm prg in
     pm
 
 let next_obligation ~pm n tac =