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.

---
 plugins/ltac/g_obligations.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/g_obligations.ml4')

diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 3e6e2db60..a301daa57 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -31,7 +31,7 @@ let () =
   Obligations.default_tactic := tac
 
 let with_tac f tac =
-  let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in
+  let env = Genintern.empty_glob_sign (Global.env ()) in
   let tac = match tac with
   | None -> None
   | Some tac ->
-- 
cgit v1.2.3