From e6b3b63eab1ca2a9586ef2c49a8df6c2e2a29adf Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 13 Jan 2014 18:38:41 +0100
Subject: rename Paral-ITP demo file

---
 test-suite/interactive/Paral-ITP.v | 41 ---------------------------------
 test-suite/interactive/ParalITP.v  | 47 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 47 insertions(+), 41 deletions(-)
 delete mode 100644 test-suite/interactive/Paral-ITP.v
 create mode 100644 test-suite/interactive/ParalITP.v

diff --git a/test-suite/interactive/Paral-ITP.v b/test-suite/interactive/Paral-ITP.v
deleted file mode 100644
index 69d3b8b882..0000000000
--- a/test-suite/interactive/Paral-ITP.v
+++ /dev/null
@@ -1,41 +0,0 @@
-(* 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 *)
-
-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. 
-  sleep time.
-  idtac.
-  sleep time.
-  (* Here we use "a" *)
-  exact a.
-Qed.
-
-Lemma work_here : True /\ True.
-Proof.
-(* Jump directly here, Coq reacts immediately *)
-split.
-  exact b.  (* We can use the lemmas above *)
-exact a.
-
diff --git a/test-suite/interactive/ParalITP.v b/test-suite/interactive/ParalITP.v
new file mode 100644
index 0000000000..a96d4a5c7f
--- /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
-- 
cgit v1.2.3