Imported Upstream version 8.5~beta1+dfsg

1 files changed, 47 insertions, 0 deletions

diff --git a/test-suite/interactive/ParalITP.v b/test-suite/interactive/ParalITP.v
new file mode 100644
index 00000000..a96d4a5c
--- /dev/null
+++ b/test-suite/interactive/ParalITP.v
@@ -0,0 +1,47 @@
+(* Some boilerplate *)
+Fixpoint fib n := match n with
+  | O => 1
+  | S m => match m with
+    | O => 1
+    | S o => fib o + fib m end end.
+
+Ltac sleep n :=
+  try (cut (fib n = S (fib n)); reflexivity).
+
+(* Tune that depending on your PC *)
+Let time := 18.
+
+
+(* Beginning of demo *)
+
+Section Demo.
+
+Variable i : True.
+
+Lemma a : True.
+Proof using i.
+  sleep time.
+  idtac.
+  sleep time.
+  (* Error, jump back to fix it, then Qed again *)
+  exact (i i).
+Qed.
+
+Lemma b : True.
+Proof using i. 
+  sleep time.
+  idtac.
+  sleep time.
+  (* Here we use "a" *)
+  exact a.
+Qed.
+
+Lemma work_here : True /\ True.
+Proof using i.
+(* Jump directly here, Coq reacts immediately *)
+split.
+  exact b.  (* We can use the lemmas above *)
+exact a.
+Qed.
+
+End Demo.
\ No newline at end of file