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

29 files changed, 127 insertions, 182 deletions

diff --git a/dev/base_include b/dev/base_include
index 0e12b57b36..d2e8f6d092 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -135,7 +135,6 @@ open Pfedit
 open Proof
 open Proof_using
 open Proof_global
-open Proof_type
 open Redexpr
 open Refiner
 open Tacmach
diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
new file mode 100644
index 0000000000..c8bea0c868
--- /dev/null
+++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then
+
+    equations_CI_REF=legacy_proof_eng_clean
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index 764d482957..e5e4f740bd 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -94,7 +94,7 @@ Tacexpr.glob_tactic_expr
  |
  | Tacinterp.eval_tactic (?)
  V
-Proof_type.tactic
+Proofview.V82.tac
 
 TODO: check with Hugo
 
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index eaa12ff702..5eac3e2b9c 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -120,9 +120,9 @@ val ppclenv : Clenv.clausenv -> unit
 
 val ppgoalgoal : Goal.goal -> unit
 
-val ppgoal : Proof_type.goal Evd.sigma -> unit
+val ppgoal : Goal.goal Evd.sigma -> unit
 (* also print evar map *)
-val ppgoalsigma : Proof_type.goal Evd.sigma -> unit
+val ppgoalsigma : Goal.goal Evd.sigma -> unit
 
 val pphintdb : Hints.Hint_db.t -> unit
 val ppproofview : Proofview.proofview -> unit
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 92fa94d6dc..ef1d1af199 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -131,8 +131,7 @@ let finish_proof dynamic_infos g =
     g
 
 
-let refine c =
-  Tacmach.refine c
+let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)
 
 let thin l = Proofview.V82.of_tactic (Tactics.clear l)
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 188d5de7de..ac2d88dec2 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -697,7 +697,7 @@ type ('b, 'c) argument_interp =
 | ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp
 | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
 | ArgInterpLegacy :
-  (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+  (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
 
 type ('a, 'b, 'c) tactic_argument = {
   arg_parsing : 'a Vernacextend.argument_rule;
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 79f9e093fb..309db539d0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -125,7 +125,7 @@ type ('b, 'c) argument_interp =
 | ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp
 | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
 | ArgInterpLegacy :
-  (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+  (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
 
 type ('a, 'b, 'c) tactic_argument = {
   arg_parsing : 'a Vernacextend.argument_rule;
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index fa58a1c39a..0a781ea8a9 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1000,7 +1000,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
           | _ -> assert false
       in loop sigma t [] n in
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
-    Tacmach.refine_no_check t gl
+    Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl
 
 let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
   let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index e92489e568..e25c93bf0a 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -164,7 +164,7 @@ val mk_lterm : constr_expr -> ssrterm
 val mk_ast_closure_term :
   [ `None | `Parens | `DoubleParens | `At ] ->
   Constrexpr.constr_expr -> ast_closure_term
-val interp_ast_closure_term : Geninterp.interp_sign -> Proof_type.goal
+val interp_ast_closure_term : Geninterp.interp_sign -> Goal.goal
 Evd.sigma -> ast_closure_term -> Evd.evar_map * ast_closure_term
 val subst_ast_closure_term : Mod_subst.substitution -> ast_closure_term -> ast_closure_term
 val glob_ast_closure_term : Genintern.glob_sign -> ast_closure_term -> ast_closure_term
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index d09b81593e..1bd88ae3dd 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -398,7 +398,7 @@ let revtoptac n0 gl =
   let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in
   let dc' = dc @ [Context.Rel.Declaration.LocalAssum(Name rev_id, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in
   let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in
-  refine (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])) gl
+  Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl
 
 let equality_inj l b id c gl =
   let msg = ref "" in
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 63b7e1783e..93a8c48435 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -230,7 +230,7 @@ sig
   val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type
   val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern
   val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern
-  val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern
+  val interp_rpattern : Geninterp.interp_sign -> Goal.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern
   val pr_rpattern : rpattern -> Pp.t
   val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern
   val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
@@ -238,7 +238,7 @@ sig
 
   val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern
   val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern
-  val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern
+  val interp_ssrterm : Geninterp.interp_sign -> Goal.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern
   val pr_ssrterm : cpattern -> Pp.t
 end
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 785f452a7b..cefc005c74 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -13,7 +13,6 @@ open Constr
 open Environ
 open Pattern
 open Evd
-open Proof_type
 open Glob_term
 open Ltac_pretype
 
@@ -144,7 +143,7 @@ val pr_transparent_state   : TransparentState.t -> Pp.t
     records containing the goal and sigma for, respectively, the new and old proof steps,
     e.g. [{ it = g ; sigma = sigma }].
 *)
-val pr_goal                : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t
+val pr_goal                : ?diffs:bool -> ?og_s:(Goal.goal sigma) -> Goal.goal sigma -> Pp.t
 
 (** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals]
    prints the goals in [goals] followed by the goals in [unfocused] in a compact form
@@ -161,17 +160,17 @@ val pr_goal                : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma ->
    there are non-instantiated existential variables.  [stack] is used to print summary info on unfocused
    goals.
 *)
-val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map
-                             -> seeds:goal list -> shelf:goal list -> stack:int list
-                             -> unfocused: goal list -> goals:goal list -> Pp.t
+val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Goal.goal Evar.Map.t) -> Pp.t option -> evar_map
+                             -> seeds:Goal.goal list -> shelf:Goal.goal list -> stack:int list
+                             -> unfocused:Goal.goal list -> goals:Goal.goal list -> Pp.t
 
-val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
+val pr_subgoal             : int -> evar_map -> Goal.goal list -> Pp.t
 
 (** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma].  The output
     is labelled "subgoal [n]".  If [diffs] is true, highlight the differences between the old conclusion,
     [og_s], and [g]+[sigma].  [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }].
 *)
-val pr_concl               : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t
+val pr_concl               : int -> ?diffs:bool -> ?og_s:(Goal.goal sigma) -> evar_map -> Goal.goal -> Pp.t
 
 (** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop.
     The first active goal is printed with all its antecedents and the conclusion.  The other active goals only show their
@@ -182,7 +181,7 @@ val pr_open_subgoals_diff  : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr
 val pr_open_subgoals       : proof:Proof.t -> Pp.t
 val pr_nth_open_subgoal    : proof:Proof.t -> int -> Pp.t
 val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
-val pr_evars_int           : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t
+val pr_evars_int           : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
 val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
   Evar.Set.t -> Pp.t
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 832393e15f..ce9ee5ae6f 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -16,7 +16,6 @@ val write_diffs_option : string -> unit
 val show_diffs : unit -> bool
 
 open Evd
-open Proof_type
 open Environ
 open Constr
 
@@ -31,7 +30,7 @@ If you want to make your call especially bulletproof, catch these
 exceptions, print a user-visible message, then recall this routine with
 the first argument set to None, which will skip the diff.
 *)
-val diff_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t
+val diff_goal_ide : Goal.goal sigma option -> Goal.goal -> Evd.evar_map -> Pp.t list * Pp.t
 
 (** Computes the diff between two goals
 
@@ -43,7 +42,7 @@ If you want to make your call especially bulletproof, catch these
 exceptions, print a user-visible message, then recall this routine with
 the first argument set to None, which will skip the diff.
 *)
-val diff_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t
+val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t
 
 (** Convert a string to a list of token strings using the lexer *)
 val tokenize_string : string -> string list
@@ -53,7 +52,7 @@ val pr_leconstr_core       : bool -> Environ.env -> Evd.evar_map -> EConstr.cons
 val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
 
 (** Computes diffs for a single conclusion *)
-val diff_concl : ?og_s:goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t
+val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t
 
 (** Generates a map from [np] to [op] that maps changed goals to their prior
 forms.  The map doesn't include entries for unchanged goals; unchanged goals
@@ -61,7 +60,7 @@ will have the same goal id in both versions.
 
 [op] and [np] must be from the same proof document and [op] must be for a state
 before [np]. *)
-val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t
+val make_goal_map : Proof.t option -> Proof.t -> Goal.goal Evar.Map.t
 
 (* Exposed for unit test, don't use these otherwise *)
 (* output channel for the test log file *)
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
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