4 files changed, 6 insertions, 74 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index b84b6db481..e09d72e474 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -46,39 +46,6 @@ type prim_rule =
 
 type rule = prim_rule
 
-type tactic_expr =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_tactic_expr
-
-and atomic_tactic_expr =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_atomic_tactic_expr
-
-and tactic_arg =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_tactic_arg
-
 (** Ltac traces *)
 
 type ltac_call_kind =
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 6688d6e621..95ca33e906 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -70,40 +70,6 @@ type goal = Goal.goal
 
 type tactic = goal sigma -> goal list sigma
 
-
-type tactic_expr =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_tactic_expr
-
-and atomic_tactic_expr =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_atomic_tactic_expr
-
-and tactic_arg =
-  (constr,
-   constr_pattern,
-   evaluable_global_reference,
-   inductive,
-   ltac_constant,
-   identifier,
-   glob_tactic_expr,
-   tlevel)
-     Tacexpr.gen_tactic_arg
-
 (** Ltac traces *)
 
 type ltac_call_kind =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 4b5bdcfe9a..33b070e765 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -23,9 +23,9 @@ 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 = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
-let abstract_tactic_expr ?(dflt=false) te tacfun = tacfun
-let abstract_tactic ?(dflt=false) te tacfun = tacfun
-let abstract_extended_tactic ?(dflt=false) s args tacfun = tacfun
+let abstract_tactic_expr tacfun = tacfun
+let abstract_tactic tacfun = tacfun
+let abstract_extended_tactic tacfun = tacfun
 
 let refiner pr goal_sigma =
   let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 6f11e71156..bc47a73c9f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -33,10 +33,9 @@ val apply_sig_tac :
 (* spiwack: currently here for compatibility, the tactic expression
    is discarded and we simply return the tactic. *)
 
-val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
-val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
-val abstract_extended_tactic :
-  ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic
+val abstract_tactic : tactic -> tactic
+val abstract_tactic_expr : tactic -> tactic
+val abstract_extended_tactic : tactic -> tactic
 
 val refiner : rule -> tactic