Generalizing the notion of constr substitution to generic arguments.

This removes a dependency on wit_tactic in Constrintern.

1 files changed, 18 insertions, 0 deletions

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