diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 12:20:04 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 12:20:04 +0000 |
| commit | 2052480ed0f065444ffb66546c450dab14b38ef4 (patch) | |
| tree | 953ffe8f04250a0e2a687a79a63392a18a9fc781 /test-suite/interactive | |
| parent | 12dce194c9b0825971d75c76e5fa944edf5b6e38 (diff) | |
Trickyer test for Paral-ITP
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16740 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/interactive')
| -rw-r--r-- | test-suite/interactive/Paral-ITP.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v index d8961c98d..55ca52bef 100644 --- a/test-suite/interactive/Paral-ITP.v +++ b/test-suite/interactive/Paral-ITP.v @@ -12,10 +12,14 @@ Let time := 15. (* BEGIN MINI DEMO *) (* JUMP TO "JUMP HERE" *) +Require Import ZArith Psatz. + 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. @@ -25,7 +29,9 @@ Proof. do 11 (cut Type; [ intro foo; clear foo | exact Type]). sleep time. idtac. - (* change in semantics: Print a. *) + assert(forall n m : Z, n + m = m + n)%Z. + intros; lia. + (* change in semantics: Print a. *) sleep time. exact a. Qed. (* JUMP HERE *) @@ -33,10 +39,13 @@ 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). |