From 05bf15c39334fa88083ab96b936d0d6f89f19d4e Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 5 Sep 2014 15:52:40 +0200
Subject: Silence an ocaml warning.

---
 tactics/tacintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6f6f144c19..9d1a9eeaf8 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 =
-- 
cgit v1.2.3