diff options
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Logic.v | 3 | ||||
-rw-r--r-- | theories/Init/Notations.v | 2 | ||||
-rw-r--r-- | theories/Init/Prelude.v | 2 | ||||
-rw-r--r-- | theories/Init/Tactics.v | 14 |
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. |