Feature request: Remove dependence of elpi on stdlib #677
Description
It would broaden the applicability of elpi if it could be used in projects compiled with the --no-init flag. I am interested in using Elpi in the Coq-HoTT library which does not use Prop anywhere and redefines equality to live in Type. Importing the stdlib is not itself fatal but one has to then be careful to avoid using any terms which are defined in the standard library.
Furthermore, if we import the stdlib it must be imported everywhere, which is annoying. It is currently not realistic/practical to import the stdlib only in the files that directly use Elpi due to a bug in the hint database system.