From 23e44c7a421d47c71318d12b1a7c5d27fb5f393a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 13 Jan 2014 18:34:59 +0100 Subject: Paral-ITP demo: better comments --- test-suite/interactive/Paral-ITP.v | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'test-suite/interactive') diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v index 658e6856f..69d3b8b88 100644 --- a/test-suite/interactive/Paral-ITP.v +++ b/test-suite/interactive/Paral-ITP.v @@ -1,3 +1,4 @@ +(* Some boilerplate *) Fixpoint fib n := match n with | O => 1 | S m => match m with @@ -7,25 +8,34 @@ Fixpoint fib n := match n with Ltac sleep n := try (cut (fib n = S (fib n)); reflexivity). +(* Tune that depending on your PC *) Let time := 18. + +(* Beginning of demo *) + Lemma a : True. Proof. sleep time. idtac. sleep time. + (* Error, jump back to fix it, then Qed again *) exact (I I). Qed. Lemma b : True. Proof. - do 11 (cut Type; [ intro foo; clear foo | exact Type]). sleep time. idtac. sleep time. + (* Here we use "a" *) exact a. Qed. -Lemma work_here : True. +Lemma work_here : True /\ True. Proof. -exact I. +(* Jump directly here, Coq reacts immediately *) +split. + exact b. (* We can use the lemmas above *) +exact a. + -- cgit v1.2.3