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

12 files changed, 16 insertions, 63 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 59feb46dc1..749eb2289c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -96,21 +96,6 @@ let is_global id =
   with Not_found ->
     false
 
-let global_reference_of_reference qid =
-  locate_reference qid
-
-let global_reference id =
-  locate_reference (qualid_of_ident id)
-
-let construct_reference ctx id =
-  try
-    VarRef (let _ = Context.Named.lookup id ctx in id)
-  with Not_found ->
-    global_reference id
-
-let global_reference_in_absolute_module dir id =
-  Nametab.global_of_path (Libnames.make_path dir id)
-
 (**********************************************************************)
 (* Internalization errors                                             *)
 
@@ -1354,7 +1339,7 @@ let sort_fields ~complete loc fields completer =
     | (first_field_ref, first_field_value):: other_fields ->
         let (first_field_glob_ref, record) =
           try
-            let gr = global_reference_of_reference first_field_ref in
+            let gr = locate_reference first_field_ref in
             (gr, Recordops.find_projection gr)
           with Not_found ->
             raise (InternalizationError(loc, NotAProjection first_field_ref))
@@ -1412,7 +1397,7 @@ let sort_fields ~complete loc fields completer =
         let rec index_fields fields remaining_projs acc =
           match fields with
             | (field_ref, field_value) :: fields ->
-               let field_glob_ref = try global_reference_of_reference field_ref
+               let field_glob_ref = try locate_reference field_ref
                with Not_found ->
                  user_err ?loc ~hdr:"intern"
                                (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2d14a0d0a7..0d4bc91f57 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -162,24 +162,11 @@ val interp_context_evars :
   env -> evar_map -> local_binder_expr list ->
   evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))
 
-(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
-(*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
-(*   ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
-  
-(* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   env -> evar_map -> local_binder_expr list ->  *)
-(*   internalization_env *  *)
-(*   ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
-
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
 
 val locate_reference :  Libnames.qualid -> GlobRef.t
 val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t
-val global_reference : Id.t -> GlobRef.t
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t
 
 (** Interprets a term as the left-hand side of a notation. The returned map is
     guaranteed to have the same domain as the input one. *)
diff --git a/parsing/dune b/parsing/dune
index e91740650f..2bb8611e09 100644
--- a/parsing/dune
+++ b/parsing/dune
@@ -2,7 +2,7 @@
  (name parsing)
  (public_name coq.parsing)
  (wrapped false)
- (libraries coq.gramlib proofs))
+ (libraries coq.gramlib interp))
 
 (rule
  (targets g_prim.ml)
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
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