Removing various compatibility layers of tactics.

1 files changed, 33 insertions, 32 deletions

diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f0471bf66..efc3dbf55 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -9,6 +9,7 @@
 open Names
 open Term
 open Environ
+open EConstr
 open Evd
 open Proof_type
 open Redexpr
@@ -40,9 +41,9 @@ val pf_nth_hyp_id         : goal sigma -> int -> Id.t
 val pf_last_hyp           : goal sigma -> Context.Named.Declaration.t
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
-val pf_unsafe_type_of            : goal sigma -> EConstr.constr -> types
-val pf_type_of            : goal sigma -> EConstr.constr -> evar_map * EConstr.types
-val pf_hnf_type_of        : goal sigma -> EConstr.constr -> EConstr.types
+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_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
@@ -50,7 +51,7 @@ val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
 val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
-val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * EConstr.constr
+val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
@@ -63,35 +64,35 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * constr
 
-val pf_whd_all       : goal sigma -> EConstr.constr -> EConstr.constr
-val pf_hnf_constr              : goal sigma -> EConstr.constr -> EConstr.constr
-val pf_nf                      : goal sigma -> EConstr.constr -> EConstr.constr
-val pf_nf_betaiota             : goal sigma -> EConstr.constr -> EConstr.constr
-val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types
-val pf_reduce_to_atomic_ind     : goal sigma -> EConstr.types -> pinductive * EConstr.types
-val pf_compute                 : goal sigma -> EConstr.constr -> EConstr.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 -> pinductive * types
+val pf_reduce_to_atomic_ind     : goal sigma -> types -> pinductive * types
+val pf_compute                 : goal sigma -> constr -> constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
-  -> goal sigma -> EConstr.constr -> EConstr.constr
+  -> goal sigma -> constr -> constr
 
 val pf_const_value : goal sigma -> pconstant -> constr
-val pf_conv_x      : goal sigma -> EConstr.constr -> EConstr.constr -> bool
-val pf_conv_x_leq  : goal sigma -> EConstr.constr -> EConstr.constr -> bool
+val pf_conv_x      : goal sigma -> constr -> constr -> bool
+val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-val pf_matches     : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool
+val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
+val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
 
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
-val internal_cut_no_check     : bool -> Id.t -> EConstr.types -> tactic
-val refine_no_check           : EConstr.constr -> tactic
+val internal_cut_no_check     : bool -> Id.t -> types -> tactic
+val refine_no_check           : constr -> tactic
 
 (** {6 The most primitive tactics with consistency and type checking } *)
 
-val internal_cut     : bool -> Id.t -> EConstr.types -> tactic
-val internal_cut_rev : bool -> Id.t -> EConstr.types -> tactic
-val refine           : EConstr.constr -> tactic
+val internal_cut     : bool -> Id.t -> types -> tactic
+val internal_cut_rev : bool -> Id.t -> types -> tactic
+val refine           : constr -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
@@ -106,11 +107,11 @@ module New : sig
 
   val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
   val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
-  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types
+  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
 
-  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types
-  val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * EConstr.types
-  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
+  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types
+  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool
 
   val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
   val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
@@ -120,16 +121,16 @@ module New : sig
   val pf_get_hyp_typ        : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
   val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
 
-  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> EConstr.types
-  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * EConstr.types
+  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
 
-  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types
-  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types
+  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
-  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr
-  val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr
+  val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map
+  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
 
   val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr