From f022907045523c0ed21750510caabc78384286bb Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Jun 2013 18:35:35 +0000
Subject: Exporting field f_debug (needed for Ssreflect).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16581 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.mli | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index a0862fe8e3..1be34a90f3 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -40,6 +40,7 @@ type interp_sign = {
   extra : TacStore.t }
 
 val f_avoid_ids : Id.t list TacStore.field
+val f_debug : debug_info TacStore.field
 
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
   Pattern.constr_under_binders Id.Map.t * (Id.Map.key * Id.t option) list
-- 
cgit v1.2.3