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


From ffac73b8f3f3bf6877ce652eecac7849b7c2a182 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Mar 2016 23:00:58 +0100
Subject: Moving Autorewrite to Hightatctic.

---
 intf/vernacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 7273b92b9a..5501ca7c7f 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -69,7 +69,6 @@ type printable =
   | PrintHint of reference or_by_notation
   | PrintHintGoal
   | PrintHintDbName of string
-  | PrintRewriteHintDbName of string
   | PrintHintDb
   | PrintScopes
   | PrintScope of string
-- 
cgit v1.2.3