Deprecate undocumented "intros until 0" in favor of "intros *".

- The case 0 makes the code of intros until (and in particular of
  Detyping.lookup_quantified_hypothesis_as_displayed more complicated).
- The introduction pattern "*" is compositional while "until 0" is not.

1 files changed, 6 insertions, 0 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index df3cca144..834d73bdd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1102,7 +1102,13 @@ let msg_quantified_hypothesis = function
       pr_nth n ++
       str " non dependent hypothesis"
 
+let warn_deprecated_intros_until_0 =
+  CWarnings.create ~name:"deprecated-intros-until-0" ~category:"tactics"
+    (fun () ->
+       strbrk"\"intros until 0\" is deprecated, use \"intros *\"; instead of \"induction 0\" and \"destruct 0\" use explicitly a name.\"")
+
 let depth_of_quantified_hypothesis red h gl =
+  if h = AnonHyp 0 then warn_deprecated_intros_until_0 ();
   match lookup_hypothesis_as_renamed_gen red h gl with
     | Some depth -> depth
     | None ->