Merge branch 'v8.5' into trunk

4 files changed, 30 insertions, 30 deletions

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index d169dc1372..07df7c7f09 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -89,25 +89,22 @@ let get_info sigma gl=
 let try_get_info sigma gl =
   Store.get (Goal.V82.extra sigma gl) info
 
-let get_stack pts =
+let get_goal_stack pts =
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
   let info = get_info sigma (List.hd goals) in
   info.pm_stack
 
 
 let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
+let proof_cond = Proof.done_cond proof_focus
 
 let focus p =
-  let inf = get_stack p in
+  let inf = get_goal_stack p in
   Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
 
 let unfocus () =
   Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
 
-let maximal_unfocus () = 
-  Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
-
 let get_top_stack pts =
   try
     Proof.get_at_focus proof_focus pts
@@ -116,6 +113,8 @@ let get_top_stack pts =
     let info = get_info sigma gl in
     info.pm_stack
 
+let get_stack pts = Proof.get_at_focus proof_focus pts
+
 let get_last env = match Environ.named_context env with
   | (id,_,_)::_ -> id
   | [] -> error "no previous statement to use"
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index 2864ba18ee..e12c4c9237 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -75,5 +75,3 @@ val get_last:  Environ.env -> Id.t
 val focus : Proof.proof -> unit
 
 val unfocus : unit -> unit
-
-val maximal_unfocus : unit -> unit
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c61079e636..ab5282e791 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -131,12 +131,13 @@ let daimon_tac gls =
 
 (* post-instruction focus management *)
 
-(* spiwack: This used to fail if there was no focusing command
-   above, but I don't think it ever happened. I hope it doesn't mess
-   things up*)
 let goto_current_focus () = 
-  Decl_mode.maximal_unfocus ()
+  Decl_mode.unfocus ()
 
+(* spiwack: used to catch errors indicating lack of "focusing command"
+   in the proof tree. In the current implementation, however, entering
+   the declarative mode puts a focus first, there should, therefore,
+   never be exception raised here. *)
 let goto_current_focus_or_top () =
   goto_current_focus ()
 
@@ -1444,12 +1445,19 @@ let rec postprocess pts instr =
 				      Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
 		  anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
 	end
-    | Pend _ ->
-	goto_current_focus_or_top ()
+    | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
+    | Pend _ -> ()
 
 let do_instr raw_instr pts =
   let has_tactic = preprocess pts raw_instr.instr in
-  begin
+  (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the
+     current proof (and, actually so does [do_instr] later one, so
+     it's ok to do the same here. Ideally the proof should be properly
+     threaded through the commands here, but since the are interleaved
+     with actions on the proof mode, which is attached to the global
+     proof environment, it is not possible without heavy lifting. *)
+  let pts = Proof_global.give_me_the_proof () in
+  let pts =
     if has_tactic then
             let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
       let gl = { it=List.hd gls ; sigma=sigma; } in
@@ -1458,13 +1466,13 @@ let do_instr raw_instr pts =
       let glob_instr = intern_proof_instr ist raw_instr in
       let instr =
 	interp_proof_instr (get_its_info gl) env sigma glob_instr in
-      ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)))
-    else () end;
-  postprocess pts raw_instr.instr;
-  (* spiwack: this should restore a compatible semantics with
-     v8.3 where we never stayed focused on 0 goal. *)
-  Proof_global.set_proof_mode "Declarative" ;
-  Decl_mode.maximal_unfocus ()
+      let (pts',_) = Proof.run_tactic (Global.env())
+        (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in
+      pts'
+    else pts
+  in
+  Proof_global.simple_with_current_proof (fun _ _ -> pts);
+  postprocess pts raw_instr.instr
 
 let proof_instr raw_instr =
   let p = Proof_global.give_me_the_proof () in
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index ef9d3159d2..2bd88d5aea 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -57,23 +57,18 @@ let vernac_decl_proof () =
   else
     begin
       Decl_proof_instr.go_to_proof_mode () ;
-      Proof_global.set_proof_mode "Declarative" ;
-      Vernacentries.print_subgoals ()
+      Proof_global.set_proof_mode "Declarative"
     end
 
 (* spiwack: some bureaucracy is not performed here *)
 let vernac_return () =
   begin
     Decl_proof_instr.return_from_tactic_mode () ;
-    Proof_global.set_proof_mode "Declarative" ;
-    Vernacentries.print_subgoals ()
+    Proof_global.set_proof_mode "Declarative"
   end
 
 let vernac_proof_instr instr =
-  begin
-    Decl_proof_instr.proof_instr instr;
-    Vernacentries.print_subgoals ()
-  end
+  Decl_proof_instr.proof_instr instr
 
 (* Before we can write an new toplevel command (see below) 
     which takes a [proof_instr] as argument, we need to declare