4 files changed, 10 insertions, 11 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index d2971552..50f853f0 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -22,9 +22,6 @@ Inductive True : Prop :=
 (** [False] is the always false proposition *)
 Inductive False : Prop :=.
 
-(** [proof_admitted] is used to implement the admit tactic *)
-Axiom proof_admitted : False.
-
 (** [not A], written [~A], is the negation of [A] *)
 Definition not (A:Prop) := A -> False.
 
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 424ca0c8..a7bdba90 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -59,7 +59,7 @@ Reserved Notation "( x , y , .. , z )" (at level 0).
 
 (** Notation "{ x }" is reserved and has a special status as component
     of other notations such as "{ A } + { B }" and "A + { B }" (which
-    are at the same level than "x + y");
+    are at the same level as "x + y");
     "{ x }" is at level 0 to factor with "{ x : A | P }" *)
 
 Reserved Notation "{ x }" (at level 0, x at level 99).
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 4894eba4..0efb8744 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -23,4 +23,4 @@ Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
 Declare ML Module "recdef_plugin".
 (* Default substrings not considered by queries like SearchAbout *)
-Add Search Blacklist "_admitted" "_subproof" "Private_".
+Add Search Blacklist "_subproof" "Private_".
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 9e828e6e..a7d3f806 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.