From 54fdae0929f2a05a89cd5c463b9a739ab2e239b8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 5 Apr 2019 02:30:45 +0200
Subject: [api] [proofs] Remove dependency of proofs on interp.

We perform some cleanup and remove dependency of `proofs/` on
`interp/`, which seems logical.

In fact, `interp` + `parsing` are quite self-contained, so if there is
interest we could also make tactics to depend directly on proofs.
---
 vernac/vernacentries.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 02db75c0f9..de8cdaa633 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1096,7 +1096,10 @@ let focus_command_cond = Proof.no_cond command_focus
      there are no more goals to solve. It cannot be a tactic since
      all tactics fail if there are no further goals to prove. *)
 
-let vernac_solve_existential ~pstate i e = Pfedit.instantiate_nth_evar_com i e pstate
+let vernac_solve_existential ~pstate n com =
+  Proof_global.simple_with_current_proof (fun _ p ->
+      let intern env sigma = Constrintern.intern_constr env sigma com in
+      Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
 
 let vernac_set_end_tac ~pstate tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
-- 
cgit v1.2.3