From 18aac5cdc6ce8be8c5c88d284cd10e82814cb303 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 04:57:00 +0200 Subject: [api] Misctypes removal: move Tactypes to proofs This gets `Tactypes` closer to `tactics/`, however some legacy stuff blocks it in `proofs`. We consider that is satisfactory for now. --- interp/genintern.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'interp/genintern.ml') diff --git a/interp/genintern.ml b/interp/genintern.ml index 161201c44..d9a0db040 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -26,9 +26,15 @@ let empty_glob_sign env = { extra = Store.empty; } +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + 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 +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct -- cgit v1.2.3