3 files changed, 34 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index bffb407274..62d3963954 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -681,13 +681,16 @@ let restrict evk filter ?candidates evd =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
       evar_extra = Store.empty } in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; evar_names }, evk'
+    defn_evars; last_mods; evar_names }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -1299,6 +1302,7 @@ let pr_decl (decl,ok) =
                            print_constr c ++ str (if ok then ")" else "}")
 
 let pr_evar_source = function
+  | Evar_kinds.NamedHole id -> pr_id id
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
   | Evar_kinds.CasesType true ->
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2fbabb7492..721389af4f 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -453,6 +453,25 @@ let iter_goal i =
   Solution.get >>= fun evd ->
   Comb.set CList.(undefined evd (flatten (rev subgoals)))
 
+(** List iter but allocates a list of results *)
+let map_goal i =
+  let rev = List.rev in (* hem... Proof masks List... *)
+  let open Proof in
+  Comb.get >>= fun initial ->
+  Proof.List.fold_left begin fun (acc, subgoals as cur) goal ->
+    Solution.get >>= fun step ->
+    match Evarutil.advance step goal with
+    | None -> return cur
+    | Some goal ->
+        Comb.set [goal] >>
+        i goal >>= fun res ->
+        Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x ->
+        return (res :: acc, x)
+  end ([],[]) initial >>= fun (results_rev, subgoals) ->
+  Solution.get >>= fun evd ->
+  Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
+  return (rev results_rev)
+
 (** A variant of [Monad.List.fold_left2] where the first list is the
     list of focused goals. The argument tactic is executed in a focus
     comprising only of the current goal, a goal which has been solved
@@ -585,7 +604,15 @@ let tclINDEPENDENT tac =
       let tac = InfoL.tag (Info.DBranch) tac in
       InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
 
-
+let tclINDEPENDENTL tac =
+  let open Proof in
+  Pv.get >>= fun initial ->
+  match initial.comb with
+  | [] -> tclUNIT []
+  | [_] -> tac >>= fun x -> return [x]
+  | _ ->
+      let tac = InfoL.tag (Info.DBranch) tac in
+      InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac))
 
 (** {7 Goal manipulation} *)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 90be2f90ab..294b03dca2 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -292,6 +292,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact
     independent of backtracking in another. It is equivalent to
     [tclEXTEND [] tac []]. *)
 val tclINDEPENDENT : unit tactic -> unit tactic
+val tclINDEPENDENTL: 'a tactic -> 'a list tactic
 
 
 (** {7 Goal manipulation} *)