From 341909bbc5c1c59e81dfad2f2532602e2561ec36 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Jan 2015 18:09:26 +0100
Subject: rename: vi -> vio

---
 test-suite/Makefile                          | 18 +++++++++---------
 test-suite/vi/simple.v                       |  2 --
 test-suite/vi/univ_constraints_statements.v  |  2 --
 test-suite/vio/simple.v                      |  2 ++
 test-suite/vio/univ_constraints_statements.v |  2 ++
 5 files changed, 13 insertions(+), 13 deletions(-)
 delete mode 100644 test-suite/vi/simple.v
 delete mode 100644 test-suite/vi/univ_constraints_statements.v
 create mode 100644 test-suite/vio/simple.v
 create mode 100644 test-suite/vio/univ_constraints_statements.v

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index d5adc4e5f9..b2f8ad79d8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -82,7 +82,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   interactive micromega $(COMPLEXITY) modules stm
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vi coqchk
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
 
 #######################################################################
 # Phony targets
@@ -99,9 +99,9 @@ bugs: $(BUGS)
 
 clean:
 	rm -f trace lia.cache
-	$(SHOW) "RM        <**/*.stamp> <**/*.vo> <**/*.vi> <**/*.log>"
+	$(SHOW) "RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>"
 	$(HIDE)find . \( \
-	  -name '*.stamp' -o -name '*.vo' -o -name '*.vi' -o -name '*.log' \
+	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \
 	\) -print0 | xargs -0 rm -f
 
 distclean: clean
@@ -140,7 +140,7 @@ summary:
 	  $(call summary_dir, "Module tests", modules); \
 	  $(call summary_dir, "STM tests", stm); \
 	  $(call summary_dir, "IDE tests", ide); \
-	  $(call summary_dir, "VI tests", vi); \
+	  $(call summary_dir, "VI tests", vio); \
 	  $(call summary_dir, "Coqchk tests", coqchk); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
@@ -428,14 +428,14 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
 	  fi; \
 	} > "$@"
 
-vi: $(patsubst %.v,%.vi.log,$(wildcard vi/*.v))
+vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
 
-%.vi.log:%.v
+%.vio.log:%.v
 	@echo "TEST      $<"
 	$(HIDE){ \
-	  $(bincoqc) -quick -R vi vi $* 2>&1 && \
-	  $(coqtop) -R vi vi -vi2vo $*.vi 2>&1 && \
-	  $(bincoqchk) -R vi vi $(subst /,.,$*) 2>&1; \
+	  $(bincoqc) -quick -R vio vio $* 2>&1 && \
+	  $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \
+	  $(bincoqchk) -R vio vio $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/vi/simple.v b/test-suite/vi/simple.v
deleted file mode 100644
index 407074c1e7..0000000000
--- a/test-suite/vi/simple.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Lemma simple : True.
-Proof using. trivial. Qed.
diff --git a/test-suite/vi/univ_constraints_statements.v b/test-suite/vi/univ_constraints_statements.v
deleted file mode 100644
index bb6b95957d..0000000000
--- a/test-suite/vi/univ_constraints_statements.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal.
-Proof using. intro H; rewrite H; trivial. Qed.
diff --git a/test-suite/vio/simple.v b/test-suite/vio/simple.v
new file mode 100644
index 0000000000..407074c1e7
--- /dev/null
+++ b/test-suite/vio/simple.v
@@ -0,0 +1,2 @@
+Lemma simple : True.
+Proof using. trivial. Qed.
diff --git a/test-suite/vio/univ_constraints_statements.v b/test-suite/vio/univ_constraints_statements.v
new file mode 100644
index 0000000000..bb6b95957d
--- /dev/null
+++ b/test-suite/vio/univ_constraints_statements.v
@@ -0,0 +1,2 @@
+Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal.
+Proof using. intro H; rewrite H; trivial. Qed.
-- 
cgit v1.2.3