Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)

based on a suggestion of Guillaume M. (done like this in ssreflect).

This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.

4 files changed, 42 insertions, 29 deletions

diff --git a/CHANGES b/CHANGES
index 96f02bc27c..70ed1bef01 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,11 @@ Specification language
 
 - Syntax "$(tactic)$" changed to "ltac:(tactic)".
 
+Tactics
+
+- Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
+  for induction.
+
 Changes from V8.5beta2 to V8.5beta3
 ===================================
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 03c4f6a365..55b5f622ff 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1531,25 +1531,27 @@ for each possible form of {\term}, i.e. one for each constructor of
 the inductive or co-inductive type. Unlike {\tt induction}, no
 induction hypothesis is generated by {\tt destruct}.
 
-If the argument is dependent in either the conclusion or some
-hypotheses of the goal, the argument is replaced by the appropriate
-constructor form in each of the resulting subgoals, thus performing
-case analysis. If non-dependent, the tactic simply exposes the
-inductive or co-inductive structure of the argument.
-
 There are special cases:
 
 \begin{itemize}
 
 \item If {\term} is an identifier {\ident} denoting a quantified
-variable of the conclusion of the goal, then {\tt destruct {\ident}}
-behaves as {\tt intros until {\ident}; destruct {\ident}}.
+  variable of the conclusion of the goal, then {\tt destruct {\ident}}
+  behaves as {\tt intros until {\ident}; destruct {\ident}}. If
+  {\ident} is not anymore dependent in the goal after application of
+  {\tt destruct}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt destruct ({\ident})}).
 
 \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt destruct} applied to the
 last introduced hypothesis. Remark: For destruction of a numeral, use
 syntax {\tt destruct ({\num})} (not very interesting anyway).
 
+\item In case {\term} is an hypothesis {\ident} of the context,
+  and {\ident} is not anymore dependent in the goal after
+  application of {\tt destruct}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt destruct ({\ident})}).
+
 \item The argument {\term} can also be a pattern of which holes are
   denoted by ``\_''. In this case, the tactic checks that all subterms
   matching the pattern in the conclusion and the hypotheses are
@@ -1626,14 +1628,6 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
   and {\tt in} clauses.
 
-\item{\tt destruct !{\ident}}
-
-  This is a case when the destructed term is an hypothesis of the
-  context. The ``!'' modifier tells to keep the hypothesis in the
-  context after destruction.
-
-  This applies also to the other form of {\tt destruct} and {\tt edestruct}.
-
 \item{\tt case \term}\label{case}\tacindex{case}
 
   The tactic {\tt case} is a more basic tactic to perform case
@@ -1699,14 +1693,22 @@ There are particular cases:
 \begin{itemize}
 
 \item If {\term} is an identifier {\ident} denoting a quantified
-variable of the conclusion of the goal, then {\tt induction {\ident}}
-behaves as {\tt intros until {\ident}; induction {\ident}}.
+  variable of the conclusion of the goal, then {\tt induction
+    {\ident}} behaves as {\tt intros until {\ident}; induction
+    {\ident}}.  If {\ident} is not anymore dependent in the goal
+  after application of {\tt induction}, it is erased (to avoid
+  erasure, use parentheses, as in {\tt induction ({\ident})}).
 
 \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt induction} applied to the
 last introduced hypothesis. Remark: For simple induction on a numeral,
 use syntax {\tt induction ({\num})} (not very interesting anyway).
 
+\item In case {\term} is an hypothesis {\ident} of the context,
+  and {\ident} is not anymore dependent in the goal after
+  application of {\tt induction}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt induction ({\ident})}).
+
 \item The argument {\term} can also be a pattern of which holes are
   denoted by ``\_''. In this case, the tactic checks that all subterms
   matching the pattern in the conclusion and the hypotheses are
@@ -1821,15 +1823,6 @@ Show 2.
   einduction}.  It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:},
   {\tt using}, and {\tt in} clauses.
 
-\item{\tt induction !{\ident}}
-
-  This is a case when the term on which to apply induction is an
-  hypothesis of the context. The ``!'' modifier tells to keep the
-  hypothesis in the context after induction.
-
-  This applies also to the other form of {\tt induction} and {\tt
-    einduction}.
-
 \item {\tt elim \term}\label{elim}
 
   This is a more basic induction tactic.  Again, the type of the
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b7559a1989..4d42dfe85a 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -44,6 +44,20 @@ let test_lpar_id_coloneq =
 	      | _ -> err ())
 	| _ -> err ())
 
+(* Hack to recognize "(x)" *)
+let test_lpar_id_rpar =
+  Gram.Entry.of_parser "lpar_id_coloneq"
+    (fun strm ->
+      match get_tok (stream_nth 0 strm) with
+        | KEYWORD "(" ->
+            (match get_tok (stream_nth 1 strm) with
+              | IDENT _ ->
+                  (match get_tok (stream_nth 2 strm) with
+	            | KEYWORD ")" -> ()
+	            | _ -> err ())
+	      | _ -> err ())
+	| _ -> err ())
+
 (* idem for (x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
   Gram.Entry.of_parser "test_lpar_idnum_coloneq"
@@ -224,8 +238,9 @@ GEXTEND Gram
   ;
   induction_arg:
     [ [ n = natural -> (None,ElimOnAnonHyp n)
+      | test_lpar_id_rpar; c = constr_with_bindings ->
+        (Some false,induction_arg_of_constr c)
       | c = constr_with_bindings -> (None,induction_arg_of_constr c)
-      | "!"; c = constr_with_bindings -> (Some false,induction_arg_of_constr c)
     ] ]
   ;
   constr_with_bindings_arg:
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 59cd25cd76..9f091e3996 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -389,7 +389,7 @@ Abort.
 
 Goal forall b:bool, True.
 intro b.
-destruct !b.
+destruct (b).
 clear b. (* b has to be here *)
 Abort.