diff options
Diffstat (limited to 'interp/genintern.mli')
| -rw-r--r-- | interp/genintern.mli | 29 |
1 files changed, 24 insertions, 5 deletions
diff --git a/interp/genintern.mli b/interp/genintern.mli index 4b244b38..d818713f 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -1,18 +1,26 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Mod_subst open Genarg +module Store : Store.S + type glob_sign = { ltacvars : Id.Set.t; - genv : Environ.env } + genv : Environ.env; + extra : Store.t; +} + +val empty_glob_sign : Environ.env -> glob_sign (** {5 Internalization functions} *) @@ -32,6 +40,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 +55,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 |