diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 6f6f144c1..9d1a9eeaf 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -628,7 +628,7 @@ and intern_tactic_seq onlytac ist = function let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in ist.ltacvars, TacAlias (loc,s,l) | TacML (loc,opn,l) -> - let () = ignore (Tacenv.interp_ml_tactic opn) in + let _ignore = Tacenv.interp_ml_tactic opn in ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_genarg ist) l) and intern_tactic_as_arg loc onlytac ist a = |