diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-05 15:52:40 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-05 18:26:01 +0200 |
| commit | 05bf15c39334fa88083ab96b936d0d6f89f19d4e (patch) | |
| tree | 8ec81ca04929cae9dfb1def8d8f00c30c1d7ecc9 /tactics | |
| parent | 64dd654dde91deb0a61e8b607673203a81cf93c0 (diff) | |
Silence an ocaml warning.
Diffstat (limited to 'tactics')
| -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 = |