[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.

8 files changed, 9 insertions, 31 deletions

diff --git a/proofs/dune b/proofs/dune
index 679c45f6bf..36e9799998 100644
--- a/proofs/dune
+++ b/proofs/dune
@@ -3,4 +3,4 @@
  (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure")
  (public_name coq.proofs)
  (wrapped false)
- (libraries interp))
+ (libraries pretyping))
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3581e90b79..a01ddf2388 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -63,7 +63,6 @@ let catchable_exception = function
   | CErrors.UserError _ | TypeError _
   | Proof.OpenProof _
   (* abstract will call close_proof inside a tactic *)
-  | Notation.PrimTokenNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 472db790f2..ef4a74b273 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -109,10 +109,6 @@ let solve ?with_end_tac gi info_lvl tac pr =
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
 
-let instantiate_nth_evar_com n com =
-  Proof_global.simple_with_current_proof (fun _ p ->
-      Proof.V82.instantiate_evar Global.(env ()) n com p)
-
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 2fe4bc6385..77d701b41f 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -54,13 +54,6 @@ val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool
 (** Option telling if unification heuristics should be used. *)
 val use_unification_heuristics : unit -> bool
 
-(** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
-   existential variable of the current focused proof by [c] or raises a
-   UserError if no proof is focused or if there is no such [n]th
-   existential variable *)
-
-val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> Proof_global.t -> Proof_global.t
-
 (** [build_by_tactic typ tac] returns a term of type [typ] by calling
     [tac]. The return boolean, if [false] indicates the use of an unsafe
     tactic. *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index e40940f652..978b1f6f78 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -480,7 +480,7 @@ module V82 = struct
       { p with proofview = Proofview.V82.grab p.proofview }
 
   (* Main component of vernac command Existential *)
-  let instantiate_evar env n com pr =
+  let instantiate_evar env n intern pr =
     let tac =
       Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
       let (evk, evi) =
@@ -494,7 +494,7 @@ module V82 = struct
           CList.nth evl (n-1)
       in
       let env = Evd.evar_filtered_env evi in
-      let rawc = Constrintern.intern_constr env sigma com in
+      let rawc = intern env sigma in
       let ltac_vars = Glob_ops.empty_lvar in
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 40e8ff7eef..defef57a8d 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -249,8 +249,11 @@ module V82 : sig
   val grab_evars : t -> t
 
   (* Implements the Existential command *)
-  val instantiate_evar :
-    Environ.env -> int -> Constrexpr.constr_expr -> t -> t
+  val instantiate_evar
+    :  Environ.env
+    -> int
+    -> (Environ.env -> Evd.evar_map -> Glob_term.glob_constr)
+    -> t -> t
 end
 
 (* returns the set of all goals in the proof *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8196f5e198..7b3d9e534b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -65,14 +65,8 @@ let pf_ids_set_of_hyps gls =
 let pf_get_new_id id gls =
   next_ident_away id (pf_ids_set_of_hyps gls)
 
-let pf_global gls id =
-  let env = pf_env gls in
-  let sigma = project gls in
-  Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id)
-
 let pf_apply f gls = f (pf_env gls) (project gls)
-let pf_eapply f gls x = 
-  on_sig gls (fun evm -> f (pf_env gls) evm x)
+let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x)
 let pf_reduce = pf_apply
 let pf_e_reduce = pf_apply
 
@@ -126,11 +120,6 @@ module New = struct
   let of_old f gl =
     f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
 
-  let pf_global id gl =
-    (* We only check for the existence of an [id] in [hyps] *)
-    let hyps = Proofview.Goal.hyps gl in
-    Constrintern.construct_reference hyps id
-
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 1454140dd7..218011c316 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -33,7 +33,6 @@ val pf_hyps_types         : Goal.goal sigma -> (Id.t Context.binder_annot * type
 val pf_nth_hyp_id         : Goal.goal sigma -> int -> Id.t
 val pf_last_hyp           : Goal.goal sigma -> named_declaration
 val pf_ids_of_hyps        : Goal.goal sigma -> Id.t list
-val pf_global             : Goal.goal sigma -> Id.t -> evar_map * constr
 val pf_unsafe_type_of     : Goal.goal sigma -> constr -> types
 val pf_type_of            : Goal.goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : Goal.goal sigma -> constr -> types
@@ -76,7 +75,6 @@ val pr_glls   : Goal.goal list sigma -> Pp.t
 module New : sig
 
   val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
-  val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t
 
   (** FIXME: encapsulate the level in an existential type. *)
   val of_old : (Goal.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a