From 16d3b231355327fa6ccc65c04790fc0415d37aef Mon Sep 17 00:00:00 2001
From: jforest
Date: Fri, 31 Aug 2007 13:19:35 +0000
Subject: fin de la correction de Function

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

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index df2755d3db..295b809697 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1016,7 +1016,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_n
 (*       (Array.make nb_goal ()) *)
 (*     ; *)
     ref := Some lemma ;
-    Options.silently (Vernacentries.interp (Vernacexpr.VernacAbort None));
+    Options.silently Vernacentries.interp (Vernacexpr.VernacAbort None);
     build_proof 
       (  fun gls ->
 	   let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in 
-- 
cgit v1.2.3