-
Notifications
You must be signed in to change notification settings - Fork 22
Enrico Tassi edited this page Jun 10, 2021
·
6 revisions
Welcome to the hierarchy-builder FAQ
-
I'm getting "Error: unable to graft this clause: no clause named compress:begin"
You need to require HB before other files using it.
From HB Require Import structures.should be the first line of every file. (This error should be gone with Coq-Elpi >= 1.10.x) -
"Error: elpi: split-at run out of list items"
Precise the types of the parameters and possibly add
#[key(T)]attribute. -
I'm getting "Error: You must declare the current class indt «axioms_» before indt «Blah.axioms_»"
You might need to amend your hierarchy with an explicit join. For a concrete illustration, see this issue. See also this dedicated page.