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.

---
 tactics/tacinterp.ml  | 2 ++
 tactics/tacinterp.mli | 2 ++
 tactics/tacsubst.ml   | 2 ++
 tactics/tacsubst.mli  | 4 ++++
 4 files changed, 10 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bf5f9ddc86..82252610a8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -44,6 +44,8 @@ open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
+let ltac_trace_info = Tacsubst.ltac_trace_info
+
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
   match Val.eq t (val_tag wit) with
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c5da3494cb..31327873e9 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -14,6 +14,8 @@ open Genarg
 open Redexpr
 open Misctypes
 
+val ltac_trace_info : ltac_trace Exninfo.t
+
 module Value :
 sig
   type t = Val.t
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 55941c1ca6..17cb8ad19b 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -18,6 +18,8 @@ open Genredexpr
 open Patternops
 open Pretyping
 
+let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
+
 (** Substitution of tactics at module closing time *)
 
 (** For generic arguments, we declare and store substitutions
diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli
index c1bf272579..8b686c5cec 100644
--- a/tactics/tacsubst.mli
+++ b/tactics/tacsubst.mli
@@ -11,6 +11,10 @@ open Mod_subst
 open Genarg
 open Misctypes
 
+(** TODO: Move those definitions somewhere sensible *)
+
+val ltac_trace_info : ltac_trace Exninfo.t
+
 (** Substitution of tactics at module closing time *)
 
 val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
-- 
cgit v1.2.3