Generalizing the notion of constr substitution to generic arguments.

This removes a dependency on wit_tactic in Constrintern.

4 files changed, 48 insertions, 14 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 630f8d140..fb11359e3 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 d6bfd347f..693101a47 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 = Tacexpr.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 4b244b38d..aabb85e00 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 = Tacexpr.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
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index f51cc3518..b1de30893 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -794,3 +794,18 @@ let () =
   Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings);
   Genintern.register_intern0 wit_destruction_arg (lift intern_destruction_arg);
   ()
+
+(** Substitution for notations containing tactic-in-terms *)
+
+let notation_subst bindings tac =
+  let fold id c accu =
+    let loc = Glob_ops.loc_of_glob_constr (fst c) in
+    let c = ConstrMayEval (ConstrTerm c) in
+    ((loc, id), c) :: accu
+  in
+  let bindings = Id.Map.fold fold bindings [] in
+  (** This is theoretically not correct due to potential variable capture, but
+      Ltac has no true variables so one cannot simply substitute *)
+  TacLetIn (false, bindings, tac)
+
+let () = Genintern.register_ntn_subst0 wit_tactic notation_subst