Make the Coq codebase independent from Ltac-related code.

We untangle many dependencies on Ltac datastructures and modules from the
lower strata, resulting in a self-contained ltac/ folder. While not a plugin
yet, the change is now very easy to perform. The main API changes have been
documented in the dev/doc/changes file.

The patches are quite rough, and it may be the case that some parts of the
code can migrate back from ltac/ to a core folder. This should be decided on
a case-by-case basis, according to a more long-term consideration of what is
exactly Ltac-dependent and whatnot.

4 files changed, 7 insertions, 8 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 13e5ea97a3..aee3405f0d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -43,6 +43,7 @@ open Glob_ops
 open Evarconv
 open Pattern
 open Misctypes
+open Tactypes
 open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -59,8 +60,6 @@ type ltac_var_map = {
 }
 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 }
 
 (************************************************************************)
 (* This concerns Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 824bb11aa4..f015813afb 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -55,9 +55,6 @@ type inference_flags = {
   expand_evars : bool
 }
 
-type 'a delayed_open =
-  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
-
 val default_inference_flags : bool -> inference_flags
 
 val no_classes_no_fail_inference_flags : inference_flags
@@ -120,7 +117,7 @@ val understand_judgment_tcc : env -> evar_map ref ->
 val type_uconstr :
   ?flags:inference_flags ->
   ?expected_type:typing_constraint ->
-  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
 
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver