From e23057ee4c492f99b09024cef5abfb49a671cfa4 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:53:11 +0000
Subject: calling interp by hand is forbidden

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

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e6f6826357..d2d5a957f4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1262,7 +1262,6 @@ 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
-    ignore (Flags.silently Vernacentries.interp (Loc.ghost,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