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

1 files changed, 40 insertions, 47 deletions

diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 14c83a6802..ef6a1544e4 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -12,85 +12,78 @@ open Names
 open Constr
 open Environ
 open EConstr
-open Proof_type
 open Redexpr
 open Locus
 
 (** Operations for handling terms under a local typing context. *)
 
 open Evd
-type tactic     = Proof_type.tactic;;
+
+type tactic = Proofview.V82.tac
 
 val sig_it  : 'a sigma   -> 'a
-val project : goal sigma -> evar_map
+val project : Goal.goal sigma -> evar_map
 
 val re_sig : 'a -> evar_map -> 'a sigma
 
-val pf_concl              : goal sigma -> types
-val pf_env                : goal sigma -> env
-val pf_hyps               : goal sigma -> named_context
-(*i val pf_untyped_hyps       : goal sigma -> (Id.t * constr) list i*)
-val pf_hyps_types         : goal sigma -> (Id.t * types) list
-val pf_nth_hyp_id         : goal sigma -> int -> Id.t
-val pf_last_hyp           : goal sigma -> named_declaration
-val pf_ids_of_hyps        : goal sigma -> Id.t list
-val pf_global             : goal sigma -> Id.t -> evar_map * constr
-val pf_unsafe_type_of            : goal sigma -> constr -> types
-val pf_type_of            : goal sigma -> constr -> evar_map * types
-val pf_hnf_type_of        : goal sigma -> constr -> types
+val pf_concl              : Goal.goal sigma -> types
+val pf_env                : Goal.goal sigma -> env
+val pf_hyps               : Goal.goal sigma -> named_context
+(*i val pf_untyped_hyps       : Goal.goal sigma -> (Id.t * constr) list i*)
+val pf_hyps_types         : Goal.goal sigma -> (Id.t * types) list
+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
 
-val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
-val pf_get_hyp_typ        : goal sigma -> Id.t -> types
+val pf_get_hyp            : Goal.goal sigma -> Id.t -> named_declaration
+val pf_get_hyp_typ        : Goal.goal sigma -> Id.t -> types
 
-val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
+val pf_get_new_id         : Id.t -> Goal.goal sigma -> Id.t
 
-val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
+val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr
 
 
-val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
+val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a
 val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> 
-  goal sigma -> 'a -> goal sigma * 'b
+  Goal.goal sigma -> 'a -> Goal.goal sigma * 'b
 val pf_reduce :
   (env -> evar_map -> constr -> constr) ->
-  goal sigma -> constr -> constr
+  Goal.goal sigma -> constr -> constr
 val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
-  goal sigma -> constr -> evar_map * constr
-
-val pf_whd_all       : goal sigma -> constr -> constr
-val pf_hnf_constr              : goal sigma -> constr -> constr
-val pf_nf                      : goal sigma -> constr -> constr
-val pf_nf_betaiota             : goal sigma -> constr -> constr
-val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types
-val pf_reduce_to_atomic_ind     : goal sigma -> types -> (inductive * EInstance.t) * types
-val pf_compute                 : goal sigma -> constr -> constr
+  Goal.goal sigma -> constr -> evar_map * constr
+
+val pf_whd_all       : Goal.goal sigma -> constr -> constr
+val pf_hnf_constr              : Goal.goal sigma -> constr -> constr
+val pf_nf                      : Goal.goal sigma -> constr -> constr
+val pf_nf_betaiota             : Goal.goal sigma -> constr -> constr
+val pf_reduce_to_quantified_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types
+val pf_reduce_to_atomic_ind     : Goal.goal sigma -> types -> (inductive * EInstance.t) * types
+val pf_compute                 : Goal.goal sigma -> constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
-  -> goal sigma -> constr -> constr
-
-val pf_const_value : goal sigma -> pconstant -> constr
-val pf_conv_x      : goal sigma -> constr -> constr -> bool
-val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
-
-(** {6 The most primitive tactics. } *)
-
-val refiner                   : rule -> tactic
-val refine_no_check           : constr -> tactic
+  -> Goal.goal sigma -> constr -> constr
 
-(** {6 The most primitive tactics with consistency and type checking } *)
-
-val refine           : constr -> tactic
+val pf_const_value : Goal.goal sigma -> pconstant -> constr
+val pf_conv_x      : Goal.goal sigma -> constr -> constr -> bool
+val pf_conv_x_leq  : Goal.goal sigma -> constr -> constr -> bool
 
 (** {6 Pretty-printing functions (debug only). } *)
-val pr_gls    : goal sigma -> Pp.t
-val pr_glls   : goal list sigma -> Pp.t
+val pr_gls    : Goal.goal sigma -> Pp.t
+val pr_glls   : Goal.goal list sigma -> Pp.t
 [@@ocaml.deprecated "Please move to \"new\" proof engine"]
 
 (** Variants of [Tacmach] functions built with the new proof engine *)
 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 : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
+  val of_old : (Goal.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
 
   val project : Proofview.Goal.t -> Evd.evar_map
   val pf_env : Proofview.Goal.t -> Environ.env