From 911cb86d51ab4f565996829b4a30cc28c52d7130 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 4 Jan 2009 18:41:02 +0000
Subject: Bug dans commit 11743

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11744 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1273d43feb..8d480ef2f2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1220,7 +1220,8 @@ let start_proof_com kind thms hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  hook strength ref) thms_data in
-      start_proof id kind t ?init_tac:rec_tac ~compute_guard:true hook
+      start_proof id kind t ?init_tac:rec_tac
+	~compute_guard:(rec_tac<>None) hook
 
 let check_anonymity id save_ident =
   if atompart_of_id id <> "Unnamed_thm" then
-- 
cgit v1.2.3