diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 18:34:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 18:54:04 +0100 |
| commit | 6ecbc9990a49a0dd51970c7fc8b13f39f02be773 (patch) | |
| tree | 027928408f8e28263edf98a5bd58cd96d43dffca /tactics | |
| parent | d3653c6da5770dfc4d439639b49193e30172763a (diff) | |
Moving Ltac traces to Tacexpr and Tacinterp.
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 |