[legacy proof engine] Remove some cruft.

We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.

This is not a lot but every little step helps.

7 files changed, 26 insertions, 26 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 63ef4f850f..b8adb792e8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -15,7 +15,6 @@ open Names
 open Constr
 open Termops
 open EConstr
-open Proof_type
 open Tacticals
 open Tacmach
 open Evd
@@ -203,7 +202,7 @@ let find_first_goal gls =
 type search_state = {
   priority : int;
   depth : int; (*r depth of search before failing *)
-  tacres : goal list sigma;
+  tacres : Goal.goal list sigma;
   last_tactic : Pp.t Lazy.t;
   dblist : hint_db list;
   localdb :  hint_db list;
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e161d88824..5aa2f42de1 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -26,7 +26,7 @@ val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list ->
 val eauto_with_bases :
   ?debug:debug ->
   bool * int ->
-  delayed_open_constr list -> hint_db list -> Proof_type.tactic
+  delayed_open_constr list -> hint_db list -> Proofview.V82.tac
 
 val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic
 val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 969f539d1f..b8967775bf 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1028,7 +1028,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
     let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
     let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
     tclTHENS (assert_after Anonymous absurd_term)
-      [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))]
+      [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))]
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
@@ -1354,8 +1354,8 @@ let inject_if_homogenous_dependent_pair ty =
         tclTHENS (cut (mkApp (ceq,new_eq_args)))
           [clear [destVar sigma hyp];
            Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
-           Proofview.V82.tactic (Tacmach.refine
-             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
+           Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
+             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
           ])]
   with Exit ->
     Proofview.tclUNIT ()
@@ -1400,7 +1400,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       (Proofview.tclIGNORE (Proofview.Monad.List.map
          (fun (pf,ty) -> tclTHENS (cut ty)
            [inject_if_homogenous_dependent_pair ty;
-            Proofview.V82.tactic (Tacmach.refine pf)])
+            Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f2cf915fe3..224cd68cf9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -26,6 +26,8 @@ module NamedDecl = Context.Named.Declaration
 (* Tacticals re-exported from the Refiner module                        *)
 (************************************************************************)
 
+type tactic = Proofview.V82.tac
+
 let tclIDTAC         = Refiner.tclIDTAC
 let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
 let tclORELSE0       = Refiner.tclORELSE0
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index cc15469d0e..2947e44f7a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -12,12 +12,13 @@ open Names
 open Constr
 open EConstr
 open Evd
-open Proof_type
 open Locus
 open Tactypes
 
 (** Tacticals i.e. functions from tactics to tactics. *)
 
+type tactic = Proofview.V82.tac
+
 val tclIDTAC         : tactic
 val tclIDTAC_MESSAGE : Pp.t -> tactic
 val tclORELSE0       : tactic -> tactic -> tactic
@@ -65,20 +66,20 @@ val onNLastHypsId    : int -> (Id.t list -> tactic) -> tactic
 val onNLastHyps      : int -> (constr list -> tactic) -> tactic
 val onNLastDecls     : int -> (named_context -> tactic) -> tactic
 
-val lastHypId   : goal sigma -> Id.t
-val lastHyp     : goal sigma -> constr
-val lastDecl    : goal sigma -> named_declaration
-val nLastHypsId : int -> goal sigma -> Id.t list
-val nLastHyps   : int -> goal sigma -> constr list
-val nLastDecls  : int -> goal sigma -> named_context
+val lastHypId   : Goal.goal sigma -> Id.t
+val lastHyp     : Goal.goal sigma -> constr
+val lastDecl    : Goal.goal sigma -> named_declaration
+val nLastHypsId : int -> Goal.goal sigma -> Id.t list
+val nLastHyps   : int -> Goal.goal sigma -> constr list
+val nLastDecls  : int -> Goal.goal sigma -> named_context
 
-val afterHyp    : Id.t -> goal sigma -> named_context
+val afterHyp    : Id.t -> Goal.goal sigma -> named_context
 
 val ifOnHyp     : (Id.t * types -> bool) ->
                   (Id.t -> tactic) -> (Id.t -> tactic) ->
 		   Id.t -> tactic
 
-val onHyps      : (goal sigma -> named_context) ->
+val onHyps      : (Goal.goal sigma -> named_context) ->
                   (named_context -> tactic) -> tactic
 
 (** {6 Tacticals applying to goal components } *)
@@ -127,11 +128,11 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis
 val compute_induction_names :
   bool list array -> or_and_intro_pattern option -> intro_patterns array
 
-val elimination_sort_of_goal : goal sigma -> Sorts.family
-val elimination_sort_of_hyp  : Id.t -> goal sigma -> Sorts.family
-val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family
+val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family
+val elimination_sort_of_hyp  : Id.t -> Goal.goal sigma -> Sorts.family
+val elimination_sort_of_clause : Id.t option -> Goal.goal sigma -> Sorts.family
 
-val pf_with_evars :  (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
+val pf_with_evars :  (Goal.goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
 val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic
 
 (** Tacticals defined directly in term of Proofview *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 349cfce205..0beafb7e31 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -142,7 +142,6 @@ let introduction id =
     | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
   end
 
-let refine          = Tacmach.refine
 let error msg = CErrors.user_err Pp.(str msg)
 
 let convert_concl ?(check=true) ty k =
@@ -1300,7 +1299,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
   if not with_evars && occur_meta clenv.evd new_hyp_typ then
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
-  let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
+  let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in
   let naming = NamingMustBe (CAst.make targetid) in
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
@@ -1624,7 +1623,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	    | Some (p,pt) ->
 	      Tacticals.New.tclTHENS
 		(assert_before_gen false (NamingAvoid avoid) pt)
-		[Proofview.V82.tactic (refine p);
+                [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p));
 		 (* Might be ill-typed due to forbidden elimination. *)
 		 Tacticals.New.onLastHypId (tac (not isrec))]
            end)))
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 4e91a9a728..75b5caaa36 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -12,7 +12,6 @@ open Names
 open Constr
 open EConstr
 open Environ
-open Proof_type
 open Evd
 open Clenv
 open Redexpr
@@ -50,8 +49,8 @@ val convert_leq     : constr -> constr -> unit Proofview.tactic
 (** {6 Introduction tactics. } *)
 
 val fresh_id_in_env : Id.Set.t -> Id.t -> env -> Id.t
-val fresh_id : Id.Set.t -> Id.t -> goal sigma -> Id.t
-val find_intro_names : rel_context -> goal sigma -> Id.t list
+val fresh_id : Id.Set.t -> Id.t -> Goal.goal sigma -> Id.t
+val find_intro_names : rel_context -> Goal.goal sigma -> Id.t list
 
 val intro                : unit Proofview.tactic
 val introf               : unit Proofview.tactic