diff options
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/utils/hierarchy.ml | 8 |
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 |