From de88278e02831707d919fe4bf8b29524230e192d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Oct 2023 16:11:32 +0200 Subject: [PATCH 1/2] Adapt to Coq PR #18007: Proof_using.definition_using takes names of recursive definitions as extra arguments. --- language-server/dm/executionManager.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 351f0eb9..4a8a2127 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -188,8 +188,10 @@ let interp_qed_delayed ~proof_using ~state_id ~st = let env = Global.env () in let sigma, _ = Declare.Proof.get_current_context proof in let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in - let terms = List.map (fun (_,_,x) -> x) (initial_goals (Declare.Proof.get proof)) in - let using = Proof_using.definition_using env sigma ~using:proof_using ~terms in + let initial_goals_pf = initial_goals (Declare.Proof.get proof) in + let terms = List.map (fun (_,_,x) -> x) initial_goals_pf in + let names = List.map (fun (id,_,_) -> id) initial_goals_pf in + let using = Proof_using.definition_using env sigma ~fixnames:names ~using:proof_using ~terms in let vars = Environ.named_context env in Names.Id.Set.iter (fun id -> if not (List.exists Util.(Context.Named.Declaration.get_id %> Names.Id.equal id) vars) then From 4e6a8552dbe27888d6f6c39fcc435230384519f0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Oct 2023 16:23:07 +0200 Subject: [PATCH 2/2] Adapt to Coq PR #18007: Proof_using.definition_using takes names of recursive definitions as extra arguments. --- language-server/dm/executionManager.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 4a8a2127..0246a072 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -183,14 +183,14 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast = (* This adapts the Future API with our event model *) let interp_qed_delayed ~proof_using ~state_id ~st = + let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in let f proof = let proof = let env = Global.env () in let sigma, _ = Declare.Proof.get_current_context proof in let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in - let initial_goals_pf = initial_goals (Declare.Proof.get proof) in - let terms = List.map (fun (_,_,x) -> x) initial_goals_pf in - let names = List.map (fun (id,_,_) -> id) initial_goals_pf in + let terms = List.map (fun (_,_,x) -> x) (initial_goals (Declare.Proof.get proof)) in + let names = Vernacstate.LemmaStack.get_all_proof_names lemmas in let using = Proof_using.definition_using env sigma ~fixnames:names ~using:proof_using ~terms in let vars = Environ.named_context env in Names.Id.Set.iter (fun id -> @@ -204,7 +204,6 @@ let interp_qed_delayed ~proof_using ~state_id ~st = let f, assign = Future.create_delegate ~blocking:false ~name:"XX" fix_exn in Declare.Proof.close_future_proof ~feedback_id:state_id proof f, assign in - let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in let proof, assign = Vernacstate.LemmaStack.with_top lemmas ~f in let control = [] (* FIXME *) in let opaque = Vernacexpr.Opaque in