From 755068fd34f0fa1e918123c4859aef2e89bedfca Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 14 Sep 2020 13:58:24 +0200
Subject: test-suite works both in local and system wide mode

---
 mathcomp/Make.test-suite | 1 -
 mathcomp/Makefile.common | 6 ++++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite
index 0b51909..f34958d 100644
--- a/mathcomp/Make.test-suite
+++ b/mathcomp/Make.test-suite
@@ -3,7 +3,6 @@ test_suite/test_ssrAC.v
 test_suite/test_guard.v
 
 -I .
--R . mathcomp
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -ambiguous-paths
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index df43b4f..b1603e6 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -58,12 +58,14 @@ Makefile.coq: pre-makefile $(COQPROJECT) Makefile
 
 ifneq "$(TEST_SKIP_BUILD)" ""
 TEST_DEP :=
+MATHCOMP_PATH := -R test_suite mathcomp.test_suite
 else
 TEST_DEP := build
+MATHCOMP_PATH := -R . mathcomp
 endif
 
 test_suite/test_hierarchy_all.v: $(TEST_DEP)
-	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp \
+	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify $(MATHCOMP_PATH) \
 		-lib all_ssreflect \
 		-lib all_algebra \
 		-lib all_field \
@@ -73,7 +75,7 @@ test_suite/test_hierarchy_all.v: $(TEST_DEP)
 		> test_suite/test_hierarchy_all.v
 
 Makefile.test-suite.coq: test_suite/test_hierarchy_all.v
-	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite -o Makefile.test-suite.coq
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite $(MATHCOMP_PATH) -o Makefile.test-suite.coq
 
 # Global config, build, clean and distclean --------------------------
 config: sub-config this-config
-- 
cgit v1.2.3