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.

1 files changed, 7 insertions, 1 deletions

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