From a899bb7ef1d6a2c35b1b9a646dfeae332972f5f6 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 26 Sep 2019 09:48:48 +0200
Subject: Fix and improve the test suite and Makefile

- improve an error message produced by the `check_join` tactic,
- fix the build of the test suite: `make test-suite`, and
- add a new rule `only` to build a subset of MathComp.
---
 etc/utils/hierarchy.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'etc')

diff --git a/etc/utils/hierarchy.ml b/etc/utils/hierarchy.ml
index 33d598a..2bb7f6f 100644
--- a/etc/utils/hierarchy.ml
+++ b/etc/utils/hierarchy.ml
@@ -159,7 +159,13 @@ Tactic Notation "check_join"
       _ (_ ?Tjoin) => Tjoin | _ ?Tjoin => Tjoin | ?Tjoin => Tjoin
     end
   in
-  is_evar Tjoin;
+  match tt with
+    | _ => is_evar Tjoin
+    | _ =>
+      let Tjoin := eval simpl in (Tjoin : Type) in
+      fail "The join of" t1 "and" t2 "is a concrete type" Tjoin
+           "but is expected to be" tjoin
+  end;
   let tjoin' := type of Tjoin in
   lazymatch tjoin' with
     | tjoin => idtac
-- 
cgit v1.2.3