From fce4a1a9cbb57a636155181898ae4ecece5af59d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Aug 2017 13:04:10 +0200
Subject: Adding the induction and destruct tactics.

---
 tests/example2.v | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

(limited to 'tests/example2.v')

diff --git a/tests/example2.v b/tests/example2.v
index d89dcfd450..812f9172c9 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -61,3 +61,37 @@ Proof.
 econstructor 1.
 split.
 Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+induction &n as [|n] using nat_rect; split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+let n := @X in
+let q := Std.NamedHyp @P in
+induction &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+destruct &n as [|n] using nat_rect; split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+let n := @X in
+let q := Std.NamedHyp @P in
+destruct &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
+Qed.
+
+Goal forall b1 b2, andb b1 b2 = andb b2 b1.
+Proof.
+intros b1 b2.
+destruct &b1 as [|], &b2 as [|]; split.
+Qed.
-- 
cgit v1.2.3