Skip to content

Commit 27ff0c0

Browse files
committed
Better error message in case of wrong structure definition order
fixes #91
1 parent c77f721 commit 27ff0c0

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

hb.elpi

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -494,8 +494,9 @@ distinct-pairs-below CurrentClass AllSuper C1 C2 :-
494494
pred assert-building-bottom-up i:class, i:classname.
495495
assert-building-bottom-up CurrentClass C3n :-
496496
class-def (class C3n X Y),
497+
CurrentClass = class CC _ _,
497498
if (not (sub-class? CurrentClass (class C3n X Y)))
498-
(coq.error "You must declare" CurrentClass "before" C3n)
499+
(coq.error "You must declare the current class" CC "before" C3n)
499500
true.
500501

501502
pred distinct-pairs_pair i:prop, o:pair class class.

0 commit comments

Comments
 (0)