Removing Proof_type from the API.

Unluckily, this forces replacing a lot of code in plugins, because the API
defined the type of goals and tactics in Proof_type, and by the no-alias rule,
this was the only one. But Proof_type was already implicitly deprecated, so
that the API should have relied on Tacmach instead.

12 files changed, 91 insertions, 91 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 0f4b86d10..94eaa1d6a 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -145,6 +145,6 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
 (* OOP : these are general shortcuts *)
 type gist = Tacintern.glob_sign
 type ist = Tacinterp.interp_sign
-type goal = Proof_type.goal 
+type goal = Goal.goal 
 type 'a sigma = 'a Evd.sigma
-type v82tac = Proof_type.tactic
+type v82tac = Tacmach.tactic
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index b0e98bdb4..20a1263d2 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -10,7 +10,7 @@
 
 open API
 
-val apply_top_tac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val inner_ssrapplytac :
   Ssrast.ssrterm list ->
@@ -19,4 +19,4 @@ val inner_ssrapplytac :
     list list ->
   Ssrast.ssrhyps ->
   Ssrast.ist ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ded9fa66b..411ce6853 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -960,7 +960,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 t));
-    Tacmach.refine_no_check (EConstr.Unsafe.to_constr t) gl
+    Tacmach.refine_no_check 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 7a4b47a46..f61168576 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -9,9 +9,9 @@
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
 open API
+open Tacmach
 open Names
 open Environ
-open Proof_type
 open Evd
 open Constrexpr
 open Ssrast
@@ -122,11 +122,11 @@ val intern_term :
     ssrterm -> Glob_term.glob_constr
 
 val pf_intern_term :
-  Tacinterp.interp_sign -> Proof_type.goal Evd.sigma ->
+  Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
     ssrterm -> Glob_term.glob_constr
 
 val interp_term :
-  Tacinterp.interp_sign -> Proof_type.goal Evd.sigma ->
+  Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
     ssrterm -> evar_map * EConstr.t
 
 val interp_wit :
@@ -136,28 +136,28 @@ val interp_hyp : ist -> goal sigma -> ssrhyp -> evar_map * ssrhyp
 val interp_hyps : ist -> goal sigma -> ssrhyps -> evar_map * ssrhyps
 
 val interp_refine :
-  Tacinterp.interp_sign -> Proof_type.goal Evd.sigma ->
+  Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
     Glob_term.glob_constr -> evar_map * (evar_map * EConstr.constr)
 
 val interp_open_constr :
-  Tacinterp.interp_sign -> Proof_type.goal Evd.sigma ->
+  Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
     Tacexpr.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t)
 
 val pf_e_type_of :
-  Proof_type.goal Evd.sigma ->
-  EConstr.constr -> Proof_type.goal Evd.sigma * EConstr.types
+  Goal.goal Evd.sigma ->
+  EConstr.constr -> Goal.goal Evd.sigma * EConstr.types
 
 val splay_open_constr : 
-           Proof_type.goal Evd.sigma ->
+           Goal.goal Evd.sigma ->
            evar_map * EConstr.t ->
            (Names.Name.t * EConstr.t) list * EConstr.t
-val isAppInd : Proof_type.goal Evd.sigma -> EConstr.types -> bool
+val isAppInd : Goal.goal Evd.sigma -> EConstr.types -> bool
 val interp_view_nbimps :
            Tacinterp.interp_sign ->
-           Proof_type.goal Evd.sigma -> Glob_term.glob_constr -> int
+           Goal.goal Evd.sigma -> Glob_term.glob_constr -> int
 val interp_nbargs :
            Tacinterp.interp_sign ->
-           Proof_type.goal Evd.sigma -> Glob_term.glob_constr -> int
+           Goal.goal Evd.sigma -> Glob_term.glob_constr -> int
 
 
 val mk_term : ssrtermkind -> 'b -> ssrtermkind * (Glob_term.glob_constr * 'b option)
@@ -169,20 +169,20 @@ val mk_internal_id : string -> Id.t
 val mk_tagged_id : string -> int -> Id.t
 val mk_evar_name : int -> Name.t
 val ssr_anon_hyp : string
-val pf_type_id :  Proof_type.goal Evd.sigma -> EConstr.types -> Id.t
+val pf_type_id :  Goal.goal Evd.sigma -> EConstr.types -> Id.t
 
 val pf_abs_evars : 
-           Proof_type.goal Evd.sigma ->
+           Goal.goal Evd.sigma ->
            evar_map * EConstr.t ->
            int * EConstr.t * Evar.t list *
            UState.t
 val pf_abs_evars2 : (* ssr2 *)
-           Proof_type.goal Evd.sigma -> Evar.t list ->
+           Goal.goal Evd.sigma -> Evar.t list ->
            evar_map * EConstr.t ->
            int * EConstr.t * Evar.t list *
            UState.t
 val pf_abs_cterm :
-           Proof_type.goal Evd.sigma -> int -> EConstr.t -> EConstr.t
+           Goal.goal Evd.sigma -> int -> EConstr.t -> EConstr.t
 
 val pf_merge_uc :
            UState.t -> 'a Evd.sigma -> 'a Evd.sigma
@@ -190,21 +190,21 @@ val pf_merge_uc_of :
            evar_map -> 'a Evd.sigma -> 'a Evd.sigma
 val constr_name : evar_map -> EConstr.t -> Name.t
 val pf_type_of :
-           Proof_type.goal Evd.sigma ->
-           Term.constr -> Proof_type.goal Evd.sigma * Term.types
+           Goal.goal Evd.sigma ->
+           Term.constr -> Goal.goal Evd.sigma * Term.types
 val pfe_type_of :
-           Proof_type.goal Evd.sigma ->
-           EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types
+           Goal.goal Evd.sigma ->
+           EConstr.t -> Goal.goal Evd.sigma * EConstr.types
 val pf_abs_prod :
            Name.t ->
-           Proof_type.goal Evd.sigma ->
+           Goal.goal Evd.sigma ->
            EConstr.t ->
-           EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types
+           EConstr.t -> Goal.goal Evd.sigma * EConstr.types
 val pf_mkprod :
-           Proof_type.goal Evd.sigma ->
+           Goal.goal Evd.sigma ->
            EConstr.t ->
            ?name:Name.t ->
-           EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types
+           EConstr.t -> Goal.goal Evd.sigma * EConstr.types
 
 val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
 val mkSsrRef : string -> Globnames.global_reference
@@ -213,15 +213,15 @@ val mkSsrConst :
            env -> evar_map -> evar_map * EConstr.t
 val pf_mkSsrConst :
            string ->
-           Proof_type.goal Evd.sigma ->
-           EConstr.t * Proof_type.goal Evd.sigma
+           Goal.goal Evd.sigma ->
+           EConstr.t * Goal.goal Evd.sigma
 val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
 
 
 val pf_fresh_global :
            Globnames.global_reference ->
-           Proof_type.goal Evd.sigma ->
-           Term.constr * Proof_type.goal Evd.sigma
+           Goal.goal Evd.sigma ->
+           Term.constr * Goal.goal Evd.sigma
 
 val is_discharged_id : Id.t -> bool
 val mk_discharged_id : Id.t -> Id.t
@@ -230,15 +230,15 @@ val has_discharged_tag : string -> bool
 val ssrqid : string -> Libnames.qualid 
 val new_tmp_id :
   tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx
-val mk_anon_id : string -> Proof_type.goal Evd.sigma -> Id.t
+val mk_anon_id : string -> Goal.goal Evd.sigma -> Id.t
 val pf_abs_evars_pirrel :
-           Proof_type.goal Evd.sigma ->
+           Goal.goal Evd.sigma ->
            evar_map * Term.constr -> int * Term.constr
-val pf_nbargs : Proof_type.goal Evd.sigma -> EConstr.t -> int
+val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int
 val gen_tmp_ids : 
            ?ist:Geninterp.interp_sign ->
-           (Proof_type.goal * tac_ctx) Evd.sigma ->
-           (Proof_type.goal * tac_ctx) list Evd.sigma
+           (Goal.goal * tac_ctx) Evd.sigma ->
+           (Goal.goal * tac_ctx) list Evd.sigma
 
 val ssrevaltac : Tacinterp.interp_sign -> Tacinterp.Value.t -> Proofview.V82.tac
 
@@ -258,23 +258,23 @@ val ssrautoprop_tac :
 val mkProt :
   EConstr.t ->
   EConstr.t ->
-  Proof_type.goal Evd.sigma ->
-  EConstr.t * Proof_type.goal Evd.sigma
+  Goal.goal Evd.sigma ->
+  EConstr.t * Goal.goal Evd.sigma
 
 val mkEtaApp : EConstr.t -> int -> int -> EConstr.t
 
 val mkRefl :
   EConstr.t ->
   EConstr.t ->
-  Proof_type.goal Evd.sigma -> EConstr.t * Proof_type.goal Evd.sigma
+  Goal.goal Evd.sigma -> EConstr.t * Goal.goal Evd.sigma
 
 val discharge_hyp :
            Id.t * (Id.t * string) ->
-           Proof_type.goal Evd.sigma -> Evar.t list Evd.sigma
+           Goal.goal Evd.sigma -> Evar.t list Evd.sigma
 
 val clear_wilds_and_tmp_and_delayed_ids :
-           (Proof_type.goal * tac_ctx) Evd.sigma ->
-           (Proof_type.goal * tac_ctx) list Evd.sigma
+           (Goal.goal * tac_ctx) Evd.sigma ->
+           (Goal.goal * tac_ctx) list Evd.sigma
 
 val view_error : string -> ssrterm -> 'a
 
@@ -284,14 +284,14 @@ val top_id : Id.t
 val pf_abs_ssrterm :
            ?resolve_typeclasses:bool ->
            ist ->
-           Proof_type.goal Evd.sigma ->
+           Goal.goal Evd.sigma ->
            ssrterm ->
            evar_map * EConstr.t * UState.t * int
 
 val pf_interp_ty :
            ?resolve_typeclasses:bool ->
            Tacinterp.interp_sign ->
-           Proof_type.goal Evd.sigma ->
+           Goal.goal Evd.sigma ->
            Ssrast.ssrtermkind *
            (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
            int * EConstr.t * EConstr.t * UState.t
@@ -309,12 +309,12 @@ exception NotEnoughProducts
 val pf_saturate :
            ?beta:bool ->
            ?bi_types:bool ->
-           Proof_type.goal Evd.sigma ->
+           Goal.goal Evd.sigma ->
            EConstr.constr ->
            ?ty:EConstr.types ->
            int ->
            EConstr.constr * EConstr.types * (int * EConstr.constr) list *
-           Proof_type.goal Evd.sigma
+           Goal.goal Evd.sigma
 val saturate :
            ?beta:bool ->
            ?bi_types:bool ->
@@ -338,32 +338,32 @@ type name_hint = (int * EConstr.types array) option ref
 val gentac : 
   (Geninterp.interp_sign ->
    (Ssrast.ssrdocc) *
-     Ssrmatching_plugin.Ssrmatching.cpattern -> Proof_type.tactic)
+     Ssrmatching_plugin.Ssrmatching.cpattern -> Tacmach.tactic)
 
 val genstac :
   ((Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) *
      Ssrmatching_plugin.Ssrmatching.cpattern)
     list * Ssrast.ssrhyp list ->
-  Tacinterp.interp_sign -> Proof_type.tactic
+  Tacinterp.interp_sign -> Tacmach.tactic
 
 val pf_interp_gen :
   Tacinterp.interp_sign ->
-  Proof_type.goal Evd.sigma ->
+  Goal.goal Evd.sigma ->
   bool ->
   (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) *
     Ssrmatching_plugin.Ssrmatching.cpattern ->
   EConstr.t * EConstr.t * Ssrast.ssrhyp list *
-    Proof_type.goal Evd.sigma
+    Goal.goal Evd.sigma
 
 val pf_interp_gen_aux :
   Tacinterp.interp_sign ->
-  Proof_type.goal Evd.sigma ->
+  Goal.goal Evd.sigma ->
   bool ->
   (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) *
     Ssrmatching_plugin.Ssrmatching.cpattern ->
   bool * Ssrmatching_plugin.Ssrmatching.pattern * EConstr.t *
     EConstr.t * Ssrast.ssrhyp list * UState.t *
-      Proof_type.goal Evd.sigma
+      Goal.goal Evd.sigma
 
 val is_name_in_ipats :
            Id.t -> ssripats -> bool
@@ -386,12 +386,12 @@ val interp_clr :
 
 val genclrtac :
   EConstr.constr ->
-  EConstr.constr list -> Ssrast.ssrhyp list -> Proof_type.tactic
+  EConstr.constr list -> Ssrast.ssrhyp list -> Tacmach.tactic
 val cleartac : ssrhyps -> v82tac
 
-val tclMULT : int * ssrmmod -> Proof_type.tactic -> Proof_type.tactic
+val tclMULT : int * ssrmmod -> Tacmach.tactic -> Tacmach.tactic
 
-val unprotecttac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+val unprotecttac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val abs_wgen :
   bool ->
@@ -401,8 +401,8 @@ val abs_wgen :
     ((Ssrast.ssrhyp_or_id * string) *
        Ssrmatching_plugin.Ssrmatching.cpattern option)
       option ->
-  Proof_type.goal Evd.sigma * EConstr.t list * EConstr.t ->
-  Proof_type.goal Evd.sigma * EConstr.t list * EConstr.t
+  Goal.goal Evd.sigma * EConstr.t list * EConstr.t ->
+  Goal.goal Evd.sigma * EConstr.t list * EConstr.t
 
 val clr_of_wgen :
   ssrhyps * ((ssrhyp_or_id * 'a) * 'b option) option ->
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli
index 8dc28d8b7..825b4758e 100644
--- a/plugins/ssr/ssrelim.mli
+++ b/plugins/ssr/ssrelim.mli
@@ -32,23 +32,23 @@ val ssrelim :
   (?ist:Ltac_plugin.Tacinterp.interp_sign ->
    'a ->
    Ssrast.ssripat option ->
-   (Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma) ->
-   bool -> Ssrast.ssrhyp list -> Proof_type.tactic) ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+   (Goal.goal Evd.sigma -> Goal.goal list Evd.sigma) ->
+   bool -> Ssrast.ssrhyp list -> Tacmach.tactic) ->
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val elimtac :
   EConstr.constr ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 val casetac :
   EConstr.constr ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
-val is_injection_case : EConstr.t -> Proof_type.goal Evd.sigma -> bool
+val is_injection_case : EConstr.t -> Goal.goal Evd.sigma -> bool
 val perform_injection :
   EConstr.constr ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val ssrscasetac :
   bool ->
   EConstr.constr ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index f712002c1..f9ab5d74f 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -25,12 +25,12 @@ val mkclr : ssrclear -> ssrdocc
 val nodocc : ssrdocc
 val noclr : ssrdocc
 
-val simpltac : Ssrast.ssrsimpl -> Proof_type.tactic
+val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic
 
 val newssrcongrtac :
   int * Ssrast.ssrterm ->
   Ltac_plugin.Tacinterp.interp_sign ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 
 val mk_rwarg :
@@ -45,7 +45,7 @@ val ssrinstancesofrule :
   Ltac_plugin.Tacinterp.interp_sign ->
   Ssrast.ssrdir ->
   Ssrast.ssrterm ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val ssrrewritetac :
   Ltac_plugin.Tacinterp.interp_sign ->
@@ -53,11 +53,11 @@ val ssrrewritetac :
      (((Ssrast.ssrhyps option * Ssrmatching.occ) *
          Ssrmatching.rpattern option) *
         (ssrwkind * Ssrast.ssrterm)))
-           list -> Proof_type.tactic
+           list -> Tacmach.tactic
 
-val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Proof_type.tactic
+val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic
 
 val unlocktac :
   Ltac_plugin.Tacinterp.interp_sign ->
   (Ssrmatching.occ * Ssrast.ssrterm) list ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index ead361745..7f254074c 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -36,7 +36,7 @@ val ssrabstract :
 
 val basecuttac :
            string ->
-           EConstr.t -> Proof_type.goal Evd.sigma -> Evar.t list Evd.sigma
+           EConstr.t -> Goal.goal Evd.sigma -> Evar.t list Evd.sigma
 
 val wlogtac :
   Ltac_plugin.Tacinterp.interp_sign ->
@@ -52,7 +52,7 @@ val wlogtac :
   Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint ->
   bool ->
   [< `Gen of Names.Id.t option option | `NoGen > `NoGen ] ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val sufftac :
   Ssrast.ist ->
@@ -62,5 +62,5 @@ val sufftac :
         (Ssrast.ssrtermkind *
            (Glob_term.glob_constr * Constrexpr.constr_expr option))) *
        (bool * Tacinterp.Value.t option list)) ->
-  Proof_type.tactic
+  Tacmach.tactic
 
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 7ae9e3824..06bbd749e 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -175,10 +175,10 @@ let move_top_with_view ~next c r v =
 
 type block_names = (int * EConstr.types array) option
 
-let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Proof_type.tactic),
+let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic),
     (tclEQINTROS : ?ind:block_names ref -> ?ist:Tacinterp.interp_sign ->
-                     Proof_type.tactic -> Proof_type.tactic -> ssripats ->
-                      Proof_type.tactic)
+                     Tacmach.tactic -> Tacmach.tactic -> ssripats ->
+                      Tacmach.tactic)
 =
 
   let rec ipattac ?ist ~next p : tac_ctx tac_a = fun gl ->
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index 5f5c7f34a..aefdc8e11 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -36,10 +36,10 @@ val elim_intro_tac :
   ?ist:Tacinterp.interp_sign ->
   [> `EConstr of 'a * 'b * EConstr.t ] ->
   Ssrast.ssripat option ->
-  Proof_type.tactic ->
+  Tacmach.tactic ->
   bool ->
   Ssrast.ssrhyp list ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 (* "move=> top; tac top; clear top" respecting the speed *)
 val with_top : (EConstr.t -> v82tac) -> tac_ctx tac_a
@@ -51,17 +51,17 @@ val ssrmovetac :
        (((Ssrast.ssrdocc * Ssrmatching.cpattern) list
         list * Ssrast.ssrclear) *
           Ssrast.ssripats)) ->
-  Proof_type.tactic
+  Tacmach.tactic
 
-val movehnftac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+val movehnftac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val with_dgens :
   (Ssrast.ssrdocc * Ssrmatching.cpattern) list
    list * Ssrast.ssrclear ->
   ((Ssrast.ssrdocc * Ssrmatching.cpattern) list ->
    Ssrast.ssrdocc * Ssrmatching.cpattern ->
-   Ltac_plugin.Tacinterp.interp_sign -> Proof_type.tactic) ->
-  Ltac_plugin.Tacinterp.interp_sign -> Proof_type.tactic
+   Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic) ->
+  Ltac_plugin.Tacinterp.interp_sign -> Tacmach.tactic
 
 val ssrcasetac :
   Ltac_plugin.Tacinterp.interp_sign ->
@@ -69,7 +69,7 @@ val ssrcasetac :
     (Ssrast.ssripat option *
        (((Ssrast.ssrdocc * Ssrmatching.cpattern) list list * Ssrast.ssrclear) *
           Ssrast.ssripats)) ->
-  Proof_type.tactic
+  Tacmach.tactic
 
 val ssrapplytac :
   Tacinterp.interp_sign ->
@@ -79,5 +79,5 @@ val ssrapplytac :
             (Ssrast.ssrtermkind * Tacexpr.glob_constr_and_expr))
            list list * Ssrast.ssrhyps) *
           Ssrast.ssripats)) ->
-  Proof_type.tactic
+  Tacmach.tactic
 
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 9207b9e43..8da9bc72b 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -12,7 +12,7 @@ open API
 open Ssrast
 
 val pp_term :
-  Proof_type.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds
+  Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds
 
 val pr_spc : unit -> Pp.std_ppcmds
 val pr_bar : unit -> Pp.std_ppcmds
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index 1d1887138..297cfdfdc 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -17,7 +17,7 @@ val tclSEQAT :
   int Misctypes.or_var *
     (('a * Ltac_plugin.Tacinterp.Value.t option list) *
        Ltac_plugin.Tacinterp.Value.t option) ->
-  Proof_type.tactic
+  Tacmach.tactic
 
 val tclCLAUSES :
   Ltac_plugin.Tacinterp.interp_sign ->
@@ -27,7 +27,7 @@ val tclCLAUSES :
         Ssrmatching_plugin.Ssrmatching.cpattern option)
        option)
     list * Ssrast.ssrclseq ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 val hinttac :
            Tacinterp.interp_sign ->
@@ -42,5 +42,5 @@ val ssrdotac :
            Ssrmatching_plugin.Ssrmatching.cpattern option)
           option)
        list * Ssrast.ssrclseq) ->
-  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 91e40f368..cc142e091 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -80,7 +80,7 @@ let interp_view ist si env sigma gv v rid =
   snd (view_with (if view_nbimps < 0 then [] else viewtab.(0)))
 
 
-let with_view ist ~next si env (gl0 : (Proof_type.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr =
+let with_view ist ~next si env (gl0 : (Goal.goal * tac_ctx) Evd.sigma) c name cl prune (conclude : EConstr.t -> EConstr.t -> tac_ctx tac_a) clr =
   let c2r ist x = { ist with lfun =
     Id.Map.add top_id (Value.of_constr x) ist.lfun } in
   let terminate (sigma, c') =