From ab7639ed91da9726f5248d9939db70df9ea18282 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 21 Dec 2018 14:14:05 -0800
Subject: Move and rewrite documentation for intro patterns that was under the
 intros tactic to its own subsection.  Add grammar and examples.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1043c50f00..070b2356e5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -98,7 +98,7 @@ let use_bracketing_last_or_and_intro_pattern () =
 
 let () =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true;
       optname  = "bracketing last or-and introduction pattern";
       optkey   = ["Bracketing";"Last";"Introduction";"Pattern"];
       optread  = (fun () -> !bracketing_last_or_and_intro_pattern);
-- 
cgit v1.2.3