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

---
 interp/constrintern.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fdd50c6a1..644cafe57 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -70,6 +70,8 @@ type ltac_sign = {
   (** Variables of Ltac which may be bound to a term *)
   ltac_bound : Id.Set.t;
   (** Other variables of Ltac *)
+  ltac_extra : Genintern.Store.t;
+  (** Arbitrary payload *)
 }
 
 val empty_ltac_sign : ltac_sign
-- 
cgit v1.2.3