From d8e0144fc1e45d72a6650461231498e65637449a Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 13 Jul 2012 08:54:02 +0000
Subject: Fixes r15610 (A new status Unsafe in Interface).

Two warnings had passed my sensors.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15619 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/recdef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index af7ec6f207..a578249738 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1289,7 +1289,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     ref_ := Some lemma ;
     let lid = ref [] in
     let h_num = ref (-1) in
-    Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None);
+    ignore (Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None));
     build_proof
       (  fun gls ->
 	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
-- 
cgit v1.2.3