From 2052480ed0f065444ffb66546c450dab14b38ef4 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Fri, 30 Aug 2013 12:20:04 +0000 Subject: Trickyer test for Paral-ITP git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16740 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/interactive/Paral-ITP.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'test-suite') 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). -- cgit v1.2.3