From 9262f440e8d8b8559c5488b1333c023f7305d811 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 23:08:19 +0100
Subject: Allowing to pass arbitrary data in internalization environments.

---
 interp/genintern.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'interp/genintern.ml')

diff --git a/interp/genintern.ml b/interp/genintern.ml
index be7abfa995..e443824bd2 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -10,9 +10,19 @@ open Names
 open Mod_subst
 open Genarg
 
+module Store = Store.Make(struct end)
+
 type glob_sign = {
   ltacvars : Id.Set.t;
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Store.t;
+}
+
+let empty_glob_sign env = {
+  ltacvars = Id.Set.empty;
+  genv = env;
+  extra = Store.empty;
+}
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
-- 
cgit v1.2.3