diff options
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 |