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.

5 files changed, 35 insertions, 36 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index ca828102b9..b8baa64019 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -7,8 +7,8 @@
 (************************************************************************)
 
 open Loc
-open Tacexpr
 open Misctypes
+open Tactypes
 open Genarg
 open Geninterp
 
@@ -30,11 +30,6 @@ let wit_int_or_var =
 let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
   make0 "intropattern"
 
-let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  make0 "tactic"
-
-let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
-
 let wit_ident =
   make0 "ident"
 
@@ -61,9 +56,6 @@ let wit_red_expr = make0 "redexpr"
 let wit_clause_dft_concl  =
   make0 "clause_dft_concl"
 
-let wit_destruction_arg =
-  make0 "destruction_arg"
-
 (** Aliases *)
 
 let wit_reference = wit_ref
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 6ccd944d43..4b542675b9 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -17,8 +17,8 @@ open Globnames
 open Genredexpr
 open Pattern
 open Constrexpr
-open Tacexpr
 open Misctypes
+open Tactypes
 open Genarg
 
 (** FIXME: nothing to do there. *)
@@ -60,20 +60,8 @@ val wit_red_expr :
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
-val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
-
-(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
-    toplevel interpretation. The one of [wit_ltac] forces the tactic and
-    discards the result. *)
-val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
-
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
 
-val wit_destruction_arg :
-  (constr_expr with_bindings destruction_arg,
-   glob_constr_and_expr with_bindings destruction_arg,
-   delayed_open_constr_with_bindings destruction_arg) genarg_type
-
 (** Aliases for compatibility *)
 
 val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 630f8d1402..fb11359e3c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -660,23 +660,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
       let arg = match arg with
       | None -> None
       | Some arg ->
-        let open Tacexpr in
-        let open Genarg in
-        let wit = glbwit Constrarg.wit_tactic in
-        let body =
-          if has_type arg wit then out_gen wit arg
-          else assert false (** FIXME *)
-        in
-        let mk_env id (c, (tmp_scope, subscopes)) accu =
+        let mk_env (c, (tmp_scope, subscopes)) =
           let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
           let gc = intern nenv c in
-          let c = ConstrMayEval (Genredexpr.ConstrTerm (gc, Some c)) in
-          ((loc, id), c) :: accu
+          (gc, Some c)
         in
-        let bindings = Id.Map.fold mk_env terms [] in
-        let tac = TacLetIn (false, bindings, body) in
-        let arg = in_gen wit tac in
-        Some arg
+        let bindings = Id.Map.map mk_env terms in
+        Some (Genintern.generic_substitute_notation bindings arg)
       in
       GHole (loc, knd, naming, arg)
     | NBinderList (x,y,iter,terminator) ->
diff --git a/interp/genintern.ml b/interp/genintern.ml
index d6bfd347ff..be7abfa995 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -16,6 +16,7 @@ type glob_sign = {
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 module InternObj =
 struct
@@ -31,8 +32,16 @@ struct
   let default _ = None
 end
 
+module NtnSubstObj =
+struct
+  type ('raw, 'glb, 'top) obj = 'glb ntn_subst_fun
+  let name = "notation_subst"
+  let default _ = None
+end
+
 module Intern = Register (InternObj)
 module Subst = Register (SubstObj)
+module NtnSubst = Register (NtnSubstObj)
 
 let intern = Intern.obj
 let register_intern0 = Intern.register0
@@ -50,3 +59,12 @@ let generic_substitute subs (GenArg (Glbwit wit, v)) =
   in_gen (glbwit wit) (substitute wit subs v)
 
 let () = Hook.set Detyping.subst_genarg_hook generic_substitute
+
+(** Notation substitution *)
+
+let substitute_notation = NtnSubst.obj
+let register_ntn_subst0 = NtnSubst.register0
+
+let generic_substitute_notation env (GenArg (Glbwit wit, v)) =
+  let v = substitute_notation wit env v in
+  in_gen (glbwit wit) v
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 4b244b38d8..4b0354be39 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -32,6 +32,14 @@ val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun
 
 val generic_substitute : glob_generic_argument subst_fun
 
+(** {5 Notation functions} *)
+
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+
+val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun
+
+val generic_substitute_notation : glob_generic_argument ntn_subst_fun
+
 (** Registering functions *)
 
 val register_intern0 : ('raw, 'glb, 'top) genarg_type ->
@@ -39,3 +47,6 @@ val register_intern0 : ('raw, 'glb, 'top) genarg_type ->
 
 val register_subst0 : ('raw, 'glb, 'top) genarg_type ->
   'glb subst_fun -> unit
+
+val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type ->
+  'glb ntn_subst_fun -> unit