From 404a8c619f76c572aec65f413baf087a374b37c3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Sep 2016 18:26:21 +0200 Subject: Generalizing the notion of constr substitution to generic arguments. This removes a dependency on wit_tactic in Constrintern. --- interp/genintern.ml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'interp/genintern.ml') 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 -- cgit v1.2.3