3 files changed, 5 insertions, 16 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index e39c066c95..b20c4d173d 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct
 | [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
 END
 
-(** Double induction *)
-
-TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
-| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
-  { Elim.h_double_induction h1 h2 }
-END
-
 (* Admit *)
 
 TACTIC EXTEND admit
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 6bf330c830..e7902d06eb 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -151,13 +151,13 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
 END
 
 VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program
-| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) }
-| [ "Obligations" ] -> { show_obligations None }
+| [ "Obligations" "of" ident(name) ] -> { fun ~stack:_ -> show_obligations (Some name) }
+| [ "Obligations" ] -> { fun ~stack:_ -> show_obligations None }
 END
 
 VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program
-| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
-| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) }
+| [ "Preterm" "of" ident(name) ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
+| [ "Preterm" ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm None) }
 END
 
 {
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index aa2449d962..937d579012 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -436,11 +436,7 @@ let finish_timing ~prefix name =
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =
-  (* The STM doesn't provide yet a proper document query and traversal
-     API, thus we need to re-check if some states are current anymore
-     (due to backtracking) using the `state_of_id` API. *)
-  let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in
-  data := SM.filter valid !data;
+  data := SM.filter (fun (doc,id) _ -> Stateid.is_valid ~doc id) !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in