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

9 files changed, 73 insertions, 130 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index c7703b52c7..4720328893 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -16,7 +16,6 @@ open EConstr
 open Refiner
 open Logic
 open Reduction
-open Tacmach
 open Clenv
 
 (* This function put casts around metavariables whose type could not be
@@ -79,7 +78,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
   let clenv = { clenv with evd = evd' } in
   tclTHEN
     (tclEVARS (Evd.clear_metas evd'))
-    (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
+    (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl
   end
 
 let clenv_pose_dependent_evars ?(with_evars=false) clenv =
diff --git a/proofs/logic.ml b/proofs/logic.ml
index f9e2edd888..15ba0a704f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -20,7 +20,6 @@ open Environ
 open Reductionops
 open Inductiveops
 open Typing
-open Proof_type
 open Type_errors
 open Retyping
 
@@ -585,12 +584,15 @@ let convert_hyp check sign sigma d =
 let prim_refiner r sigma goal =
   let env = Goal.V82.env sigma goal in
   let cl = Goal.V82.concl sigma goal in
-  match r with
-    (* Logical rules *)
-    | Refine c ->
-        let cl = EConstr.Unsafe.to_constr cl in
-        check_meta_variables env sigma c;
-	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
-	let sgl = List.rev sgl in
-        let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
-	  (sgl, sigma)
+  let cl = EConstr.Unsafe.to_constr cl in
+  check_meta_variables env sigma r;
+  let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in
+  let sgl = List.rev sgl in
+  let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
+  (sgl, sigma)
+
+let prim_refiner ~check r sigma goal =
+  if check then
+    with_check (prim_refiner r sigma) goal
+  else
+    prim_refiner r sigma goal
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2cad278e10..f99076db23 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -13,27 +13,20 @@
 open Names
 open Constr
 open Evd
-open Proof_type
 
-(** This suppresses check done in [prim_refiner] for the tactic given in
-   argument; works by side-effect *)
-
-val with_check    : tactic -> tactic
-
-(** [without_check] respectively means:\\
-  [Intro]: no check that the name does not exist\\
-  [Intro_after]: no check that the name does not exist and that variables in
+(** [check] respectively means:\\
+  [Intro]: check that the name does not exist\\
+  [Intro_after]: check that the name does not exist and that variables in
      its type does not escape their scope\\
-  [Intro_replacing]: no check that the name does not exist and that
+  [Intro_replacing]: check that the name does not exist and that
      variables in its type does not escape their scope\\
   [Convert_hyp]:
-  no check that the name exist and that its type is convertible\\
+  check that the name exist and that its type is convertible\\
 *)
 
 (** The primitive refiner. *)
 
-val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
-
+val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map
 
 (** {6 Refiner errors. } *)
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
deleted file mode 100644
index 149f30c673..0000000000
--- a/proofs/proof_type.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Legacy proof engine. Do not use in newly written code. *)
-
-open Evd
-open Constr
-
-(** This module defines the structure of proof tree and the tactic type. So, it
-   is used by [Proof_tree] and [Refiner] *)
-
-type prim_rule =
-  | Refine of constr
-
-(** Nowadays, the only rules we'll consider are the primitive rules *)
-
-type rule = prim_rule
-
-type goal = Goal.goal
-
-type tactic = goal sigma -> goal list sigma
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index f9bb2c3d60..dbd5be23ab 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,7 +1,6 @@
 Miscprint
 Goal
 Evar_refiner
-Proof_type
 Refine
 Proof
 Logic
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index be32aadd91..bce227dabb 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -12,9 +12,10 @@ open Pp
 open CErrors
 open Util
 open Evd
-open Proof_type
 open Logic
 
+type tactic = Proofview.V82.tac
+
 module NamedDecl = Context.Named.Declaration
 
 let sig_it x = x.it
@@ -25,16 +26,16 @@ let project x = x.sigma
 let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
 let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
-let refiner pr goal_sigma =
-  let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
+let refiner ~check pr goal_sigma =
+  let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in
   { it = sgl; sigma = sigma'; }
 
 (* Profiling refiner *)
-let refiner = 
+let refiner ~check =
   if Flags.profile then
     let refiner_key = CProfile.declare_profile "refiner" in
-      CProfile.profile2 refiner_key refiner
-  else refiner
+      CProfile.profile2 refiner_key (refiner ~check)
+  else refiner ~check
 
 (*********************)
 (*   Tacticals       *)
@@ -178,9 +179,9 @@ let tclPROGRESS tac ptree =
    NOTE: some tactics delete hypothesis and reuse names (induction,
    destruct), this is not detected by this tactical. *)
 let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
-    :Proof_type.goal list Evd.sigma =
+    : Goal.goal list Evd.sigma =
   let oldhyps = pf_hyps goal in
-  let rslt:Proof_type.goal list Evd.sigma = tac goal in
+  let rslt:Goal.goal list Evd.sigma = tac goal in
   let { it = gls; sigma = sigma; } = rslt in
   let hyps =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 30af6d8e1a..52cbf7658b 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -11,18 +11,18 @@
 (** Legacy proof engine. Do not use in newly written code. *)
 
 open Evd
-open Proof_type
 open EConstr
 
 (** The refiner (handles primitive rules and high-level tactics). *)
+type tactic = Proofview.V82.tac
 
 val sig_it  : 'a sigma -> 'a
 val project : 'a sigma -> evar_map
 
-val pf_env  : goal sigma -> Environ.env
-val pf_hyps : goal sigma -> named_context
+val pf_env  : Goal.goal sigma -> Environ.env
+val pf_hyps : Goal.goal sigma -> named_context
 
-val refiner : rule -> tactic
+val refiner : check:bool -> Constr.t -> tactic
 
 (** {6 Tacticals. } *)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 231a8fe266..64d7630d55 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -17,9 +17,7 @@ open Evd
 open Typing
 open Redexpr
 open Tacred
-open Proof_type
 open Logic
-open Refiner
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -30,7 +28,7 @@ let re_sig it  gc = { it = it; sigma = gc; }
 (* Operations for handling terms under a local typing context *)
 (**************************************************************)
 
-type tactic     = Proof_type.tactic
+type tactic = Proofview.V82.tac
 
 let sig_it   = Refiner.sig_it
 let project  = Refiner.project
@@ -103,20 +101,6 @@ let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
-(********************************************)
-(* Definition of the most primitive tactics *)
-(********************************************)
-
-let refiner = refiner
-
-let refine_no_check c gl =
-  let c = EConstr.Unsafe.to_constr c in
-  refiner (Refine c) gl
-
-(* Versions with consistency checks *)
-
-let refine c           = with_check (refine_no_check c)
-
 (* Pretty-printers *)
 
 open Pp
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