From 6ecbc9990a49a0dd51970c7fc8b13f39f02be773 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Mar 2016 18:34:39 +0100
Subject: Moving Ltac traces to Tacexpr and Tacinterp.

---
 intf/tacexpr.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index f2a567c00d..b1dc174d4b 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -394,3 +394,15 @@ type tactic_arg =
 
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
 type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
+
+(** Traces *)
+
+type ltac_call_kind =
+  | LtacMLCall of glob_tactic_expr
+  | LtacNotationCall of KerName.t
+  | LtacNameCall of ltac_constant
+  | LtacAtomCall of glob_atomic_tactic_expr
+  | LtacVarCall of Id.t * glob_tactic_expr
+  | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
+
+type ltac_trace = (Loc.t * ltac_call_kind) list
-- 
cgit v1.2.3