Info: dispatching-branches are declared as such in the info trace.

Hence dispatches are printed as dispatches rather than sequences.

1 files changed, 15 insertions, 3 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d55689a202..e03249ca56 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -436,7 +436,7 @@ let fold_left2_goal i s l =
     successive results of [tacs] are stored in reverse order in a
     list, and [join] is used to convert the result into the expected
     form. *)
-let tclDISPATCHGEN join tacs =
+let tclDISPATCHGEN0 join tacs =
   match tacs with
   | [] ->
       begin 
@@ -461,6 +461,11 @@ let tclDISPATCHGEN join tacs =
       let ans = fold_left2_goal iter [] tacs in
       Proof.map join ans
 
+let tclDISPATCHGEN join tacs =
+  let branch t = InfoL.tag (Info.DBranch) t in
+  let tacs = CList.map branch tacs in
+  InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs)
+
 let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs
 
 let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs
@@ -515,7 +520,9 @@ let tclINDEPENDENT tac =
   match initial.comb with
   | [] -> tclUNIT ()
   | [_] -> tac
-  | _ -> iter_goal (fun _ -> tac)
+  | _ ->
+      let tac = InfoL.tag (Info.DBranch) tac in
+      InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
 
 
 
@@ -827,16 +834,18 @@ module Goal = struct
     gmake_with info env sigma goal , sigma
 
   let nf_enter f =
+    InfoL.tag (Info.Dispatch) begin
     iter_goal begin fun goal ->
       Env.get >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in
-        tclTHEN (Unsafe.tclEVARS sigma) (f gl)
+        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
       with e when catchable_exception e ->
         let e = Errors.push e in
         tclZERO e
     end
+    end
 
   let normalize { self } =
     Env.get >>= fun env ->
@@ -849,6 +858,8 @@ module Goal = struct
     gmake_with info env sigma goal
 
   let enter f =
+    let f gl = InfoL.tag (Info.DBranch) (f gl) in
+    InfoL.tag (Info.Dispatch) begin
     iter_goal begin fun goal ->
       Env.get >>= fun env ->
       tclEVARMAP >>= fun sigma ->
@@ -857,6 +868,7 @@ module Goal = struct
         let e = Errors.push e in
         tclZERO e
     end
+    end
 
   let goals =
     Env.get >>= fun env ->