From 0583805fa794380eb9031e2c8a147fee7facacf0 Mon Sep 17 00:00:00 2001
From: vsiles
Date: Tue, 4 May 2010 16:56:40 +0000
Subject:   - Fixing bug #2308 about Lemma ... with   - Fixing a wierd
 behaviour of the goal window (scroll_at_iter doesn't work)

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

(limited to 'toplevel/command.ml')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index fcc6c8acea..3e16a956a0 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -547,7 +547,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
     Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
-      (Some(false,indexes,init_tac)) thms (fun _ _ -> ())
+      (Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -572,7 +572,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
     Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
-      (Some(true,[],init_tac)) thms (fun _ _ -> ())
+      (Some(true,[],init_tac)) thms None (fun _ _ -> ())
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
-- 
cgit v1.2.3