From 1b43dfcb6facbc88c611db3ecb9076e377eebb34 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 29 Nov 2020 00:10:07 +0100 Subject: Removing flag "Bracketing Last Introduction Pattern". --- doc/sphinx/proof-engine/tactics.rst | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8f5c045929..d8c4fb61c2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -264,17 +264,6 @@ These patterns can be used when the hypothesis is an equality: :n:`@simple_intropattern_closed`. :ref:`Example ` -.. flag:: Bracketing Last Introduction Pattern - - For :n:`intros @intropattern_list`, controls how to handle a - conjunctive pattern that doesn't give enough simple patterns to match - all the arguments in the constructor. If set (the default), Coq generates - additional names to match the number of arguments. - Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more - similar to |SSR|'s intro patterns. - - .. deprecated:: 8.10 - .. _intropattern_cons_note: .. note:: -- cgit v1.2.3