Merge branch 'v8.5'

2 files changed, 18 insertions, 16 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9e828e6ea0..a7d3f8062a 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -180,12 +180,14 @@ Ltac easy :=
     | H : _ |- _ => solve [inversion H]
     | _ => idtac
     end in
-  let rec do_atom :=
-    solve [reflexivity | symmetry; trivial] ||
-    contradiction ||
-    (split; do_atom)
-  with do_ccl := trivial with eq_true; repeat do_intro; do_atom in
-  (use_hyps; do_ccl) || fail "Cannot solve this goal".
+  let do_atom :=
+    solve [ trivial with eq_true | reflexivity | symmetry; trivial | contradiction ] in
+  let rec do_ccl :=
+    try do_atom;
+    repeat (do_intro; try do_atom);
+    solve [ split; do_ccl ] in
+  solve [ do_atom | use_hyps; do_ccl ] ||
+  fail "Cannot solve this goal".
 
 Tactic Notation "now" tactic(t) := t; easy.
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 4b02873172..ae6fe7dd0a 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -433,40 +433,40 @@ Ltac do_depelim' rev tac H :=
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
 
-Tactic Notation "dependent" "destruction" hyp(H) := 
+Tactic Notation "dependent" "destruction" ident(H) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" hyp(H) "using" constr(c) := 
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => destruct hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the elimination. *)
 
-Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) := 
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H.
 
 (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
    writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before
    calling [induction]. *)
 
-Tactic Notation "dependent" "induction" hyp(H) :=
+Tactic Notation "dependent" "induction" ident(H) :=
   do_depind ltac:(fun hyp => do_ind hyp) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "using" constr(c) :=
+Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
   do_depind ltac:(fun hyp => induction hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
-Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) := 
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_ind hyp) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) :=
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) :=
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l) H.
 
-Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l using c) H.