diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 | ||||
| -rw-r--r-- | tactics/tacsubst.mli | 4 |
4 files changed, 10 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index bf5f9ddc8..82252610a 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 c5da3494c..31327873e 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 55941c1ca..17cb8ad19 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 c1bf27257..8b686c5ce 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 |