tactic notations (#31)

1 files changed, 8 insertions, 7 deletions

diff --git a/examples/Example.v b/examples/Example.v
index f7877b7..4b2fda9 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -152,6 +152,7 @@ Proof.
   smt.
 Qed.
 
+(* From cvc4_bool : Uncaught exception Not_found *)
 (* Goal forall (a b c d: farray Z Z), *)
 (*     b[0 <- 4] = c  -> *)
 (*     d = b[0 <- 4][1 <- 4]  -> *)
@@ -258,7 +259,7 @@ Qed.
 
 Open Scope Z_scope.
 
-(* Some examples of using verit with lemmas. Use <verit_base H1 .. Hn; vauto>
+(* Some examples of using verit with lemmas. Use <verit H1 .. Hn>
    to temporarily add the lemmas H1 .. Hn to the verit environment. *)
 Lemma const_fun_is_eq_val_0 :
   forall f : Z -> Z,
@@ -266,7 +267,7 @@ Lemma const_fun_is_eq_val_0 :
     forall x, f x =? f 0.
 Proof.
   intros f Hf.
-  verit_bool_base Hf; vauto.
+  verit Hf.
 Qed.
 
 Section Without_lemmas.
@@ -285,7 +286,7 @@ Section With_lemmas.
 
   Lemma fSS2:
     forall x, f (x + 2) =? f x + 2 * k.
-  Proof. verit_bool_base f_k_linear; vauto. Qed.
+  Proof. verit f_k_linear. Qed.
 End With_lemmas.
 
 (* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to
@@ -310,7 +311,7 @@ Section NonLinear.
     (mult (3 + a) b =? mult 3 b + mult a b).
   Proof.
     intro H.
-    verit_bool_base H; vauto.
+    verit H.
   Qed.
 End NonLinear.
 
@@ -337,14 +338,14 @@ Section group.
 
   Lemma unique_identity e':
     (forall z, op e' z =? z) -> e' =? e.
-  Proof. intros pe'. verit_bool_base pe'; vauto. Qed.
+  Proof. intros pe'. verit pe'. Qed.
   Lemma simplification_right x1 x2 y:
       op x1 y =? op x2 y -> x1 =? x2.
-  Proof. intro H. verit_bool_base H; vauto. Qed.
+  Proof. intro H. verit H. Qed.
 
   Lemma simplification_left x1 x2 y:
       op y x1 =? op y x2 -> x1 =? x2.
-  Proof. intro H. verit_bool_base H; vauto. Qed.
+  Proof. intro H. verit H. Qed.
 
   Clear_lemmas.
 End group.