Unplugging Tacexpr in several interface files.

4 files changed, 8 insertions, 2 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 886a982634..5ec44a68d8 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -45,6 +45,7 @@ open Context.Rel.Declaration
 
  *)
 
+type binding_bound_vars = Id.Set.t
 type bound_ident_map = Id.t Id.Map.t
 
 exception PatternMatchingFailure
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 8d8166f22f..ee6c5141b0 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -13,6 +13,8 @@ open Term
 open Environ
 open Pattern
 
+type binding_bound_vars = Id.Set.t
+
 (** [PatternMatchingFailure] is the exception raised when pattern
   matching fails *)
 exception PatternMatchingFailure
@@ -41,7 +43,7 @@ val matches_head : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
    variables or metavariables have the same name, the metavariable,
    or else the rightmost bound variable, takes precedence *)
 val extended_matches :
-  env -> Evd.evar_map -> Tacexpr.binding_bound_vars * constr_pattern ->
+  env -> Evd.evar_map -> binding_bound_vars * constr_pattern ->
   constr -> bound_ident_map * extended_patvar_map
 
 (** [is_matching pat c] just tells if [c] matches against [pat] *)
@@ -75,7 +77,7 @@ val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matchi
 (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
 val match_subterm_gen : env -> Evd.evar_map ->
   bool (** true = with app context *) ->
-  Tacexpr.binding_bound_vars * constr_pattern -> constr ->
+  binding_bound_vars * constr_pattern -> constr ->
   matching_result IStream.t
 
 (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 385e100e2d..0d9bde2ec2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -61,6 +61,7 @@ type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 type 'a delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
+type delayed_open_constr = constr delayed_open
 
 (************************************************************************)
 (* This concerns Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 824bb11aa4..7cb256e4fb 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -58,6 +58,8 @@ type inference_flags = {
 type 'a delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
+type delayed_open_constr = constr delayed_open
+
 val default_inference_flags : bool -> inference_flags
 
 val no_classes_no_fail_inference_flags : inference_flags