1 files changed, 0 insertions, 33 deletions
diff --git a/Tutorial.v b/Tutorial.v
index 6356a10..76006ca 100644
--- a/Tutorial.v
+++ b/Tutorial.v
@@ -397,36 +397,3 @@ Section Examples.
 End Examples.
 
 
-Section Match. 
-  (* The following example is inspired by a question by Francois
-  Pottier, wokring in the context of separation logic. *)
-
-  Variable T : Type. 
-  Variable star : T -> T -> T. 
-  Hypothesis P : T -> Prop. 
-
-  Context (starA : Associative eq star).   
-  Context (starC : Commutative eq star).   
-
-  Hypothesis P_hereditary_left : forall a b, P (star a b) -> P a. 
-  Hypothesis P_hereditary_right : forall a b, P (star a b) -> P b. 
-  
-  Notation "a * b" := (star a b). 
-
-  Ltac crush :=
-    match goal with 
-        H: P ?R' |- P ?R =>
-        let h := fresh in
-        aac_match (fun x => x * R) R' h;
-          rewrite <- h in H;
-          try eauto using P_hereditary_right
-    end.    
-
-  Goal forall a b c, P (c * a * c * b) -> P (b * a). 
-  Proof. intros.  crush.  Qed. 
-
-  Goal forall a b c, exists d,  P (d * a * c * b) -> P (b * d) /\ b = d. 
-  Proof. intros.  eexists. intros.  split. crush. reflexivity. Qed. 
-
-End Match. 
-