From bd76e995548d23100f2dbe7f5d13047402eb8251 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 13 Jan 2014 18:29:35 +0100
Subject: STM: fix very simple demo

---
 test-suite/interactive/Paral-ITP.v | 83 ++------------------------------------
 1 file changed, 3 insertions(+), 80 deletions(-)

(limited to 'test-suite/interactive')

diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v
index 55ca52bef..658e6856f 100644
--- a/test-suite/interactive/Paral-ITP.v
+++ b/test-suite/interactive/Paral-ITP.v
@@ -7,19 +7,12 @@ Fixpoint fib n := match n with
 Ltac sleep n :=
   try (cut (fib n = S (fib n)); reflexivity).
 
-Let time := 15.
-
-(* BEGIN MINI DEMO *)
-(* JUMP TO "JUMP HERE" *)
-
-Require Import ZArith Psatz.
+Let time := 18.
 
 Lemma a : True.
 Proof.
   sleep time.
   idtac.
-  assert(forall n m : Z, n + m = m + n)%Z.
-    intros; lia.
   sleep time.
   exact (I I).
 Qed.
@@ -29,80 +22,10 @@ Proof.
   do 11 (cut Type; [ intro foo; clear foo | exact Type]).
   sleep time.
   idtac.
-  assert(forall n m : Z, n + m = m + n)%Z.
-    intros; lia.
- (* change in semantics: Print a. *)
   sleep time.
   exact a.
-Qed. (* JUMP HERE *)
-
-Lemma work_here : True.
-Proof.
-cut True.
-Print b.
-Abort.
-
-(* END MINI DEMO *)
-
-
-
-Require Import Unicode.Utf8.
-Notation "a ⊃ b" := (a → b) (at level 91, left associativity).
-
-Definition untrue := False.
-
-Section Ex.
-Variable P Q : Prop.
-Implicit Types X Y : Prop.
-Hypothesis CL : forall X Y, (X → ¬Y → untrue) → (¬X ∨ Y).
-
-Lemma  Peirce : P ⊃ Q ⊃ P ⊃ P.
-Proof (* using P Q CL. *).   (* Uncomment -> more readable *)
-intro pqp.
-
-  Remark EM : ¬P ∨ P.
-  Proof using P CL.
-  intros; apply CL; intros p np.
-  Fail progress auto.  (* Missing hint *)
-
-  (* Try commenting this out *)
-  Hint Extern 0 => match goal with
-    p : P, np : ¬P |- _ => case (np p)
-  end.
-
-  auto.  (* This line requires the hint above *)
-  Qed.
-
-case EM; auto.  (* This line requires the hint above *)
 Qed.
 
-End Ex.
-
-Check EM. (* Print EM. *)
-
-
-Axiom exM : forall P, P \/ ~P.
-
-Lemma CPeirce (P Q : Prop) : P ⊃ Q ⊃ P ⊃ P.
-Proof.
-apply Peirce.
-intros.
-case (exM X); auto.
-intro; right.
-case (exM Y); auto; intro.
-case H; auto.
-Qed.
-
-Require Import Recdef.
-
-Definition m (n : nat) := n.
-
-Function f (n : nat) {measure m n} : bool :=
-  match n with
-  | O => true
-  | S x => f (x + 0)
-  end.
+Lemma work_here : True.
 Proof.
-intros x y _. unfold m.
-rewrite <- plus_n_O. auto.
-Qed.
+exact I.
-- 
cgit v1.2.3