From fc1b3ef9d7270938cd83c524aae0383093b7a4b5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 27 Feb 2015 20:42:44 +0100
Subject: Removing the unused field ltacrecvars of tactic internalization.

---
 interp/genintern.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/genintern.ml')

diff --git a/interp/genintern.ml b/interp/genintern.ml
index c78b13a8f..7795946d5 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -12,7 +12,6 @@ open Genarg
 
 type glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : Nametab.ltac_constant Id.Map.t;
   genv : Environ.env }
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
-- 
cgit v1.2.3