diff options
Diffstat (limited to 'tactics/tacsubst.ml')
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 17cb8ad19..55941c1ca 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -18,8 +18,6 @@ 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 |