From dd6c458085d4050411fa4bd1ad4aca26e4145950 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:59:50 +0200
Subject: refactor: Rename test file

---
 ci/coq-tests.el    |  8 ++++----
 ci/test1.v         | 22 ----------------------
 ci/test_stepwise.v | 22 ++++++++++++++++++++++
 3 files changed, 26 insertions(+), 26 deletions(-)
 delete mode 100644 ci/test1.v
 create mode 100644 ci/test_stepwise.v

(limited to 'ci')

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index e88736e9..ac97a110 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -181,7 +181,7 @@ For example, COMMENT could be (*test-definition*)"
 (ert-deftest 020_coq-test-definition ()
   "Test *response* output after asserting a Definition."
   (coq-fixture-on-file
-   (coq-test-full-path "test1.v")
+   (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before "(*test-definition*)")
      (proof-goto-point)
@@ -192,7 +192,7 @@ For example, COMMENT could be (*test-definition*)"
 (ert-deftest 030_coq-test-position ()
   "Test locked region after Qed."
   (coq-fixture-on-file
-   (coq-test-full-path "test1.v")
+   (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma*)")
      (let ((proof-point (point)))
@@ -204,7 +204,7 @@ For example, COMMENT could be (*test-definition*)"
 (ert-deftest 040_coq-test-insert ()
   "Test retract on insert from Qed."
   (coq-fixture-on-file
-   (coq-test-full-path "test1.v")
+   (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma*)")
      (proof-goto-point)
@@ -220,7 +220,7 @@ For example, COMMENT could be (*test-definition*)"
 (ert-deftest 050_coq-test-lemma-false ()
   "Test retract on proof error."
   (coq-fixture-on-file
-   (coq-test-full-path "test1.v")
+   (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma2*)")
      (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) 
diff --git a/ci/test1.v b/ci/test1.v
deleted file mode 100644
index 3812adbd..00000000
--- a/ci/test1.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Definition trois := 3. (*test-definition*)
-Print trois.
-Eval compute in 10 * trois * trois.
- 
-
-
-Lemma easy_proof : forall A : Prop, A -> A.
-Proof using .
-  intros A.
-  intros proof_of_A. (*test-insert*)
-  exact proof_of_A.
-Qed. (*test-lemma*)
-
-Lemma false_proof : forall A B : bool, A = B. 
-Proof.
-  intros A B.
-  destruct A.
-  destruct B.
-  reflexivity. (*error*)
-  reflexivity.
-Qed. (*test-lemma2*)
-  
diff --git a/ci/test_stepwise.v b/ci/test_stepwise.v
new file mode 100644
index 00000000..3812adbd
--- /dev/null
+++ b/ci/test_stepwise.v
@@ -0,0 +1,22 @@
+Definition trois := 3. (*test-definition*)
+Print trois.
+Eval compute in 10 * trois * trois.
+ 
+
+
+Lemma easy_proof : forall A : Prop, A -> A.
+Proof using .
+  intros A.
+  intros proof_of_A. (*test-insert*)
+  exact proof_of_A.
+Qed. (*test-lemma*)
+
+Lemma false_proof : forall A B : bool, A = B. 
+Proof.
+  intros A B.
+  destruct A.
+  destruct B.
+  reflexivity. (*error*)
+  reflexivity.
+Qed. (*test-lemma2*)
+  
-- 
cgit v1.2.3