Don't Require PrimInt63 and PrimFloat by default #579
Conversation
| @@ -84,11 +93,11 @@ GRAMMAR EXTEND Gram | |||
|
|
|||
| term: LEVEL "0" | |||
| [ [ "lib"; ":"; id = qualified_name -> { | |||
| let ref = Coqlib.lib_ref (String.concat "." (snd id)) in | |||
| let ref = lib_ref id in | |||
| let path = Nametab.path_of_global ref in | |||
There was a problem hiding this comment.
not really related to this PR but looking up lib_ref and nametab during parsing is pretty bad with parsing/execution separated
There was a problem hiding this comment.
Actually, this is really tricky. I do extend the Coq grammar, so there is a bug, but we only use it inside elpi code, hence inside a quotation. The text between {{ ... }} is parsed as a string, and the Coq parser is called at run time. So I think it is mostly fine for the use we make.
Anyway, lib: predates the ability of elpi to compile units, we don't need that anymore. So maybe it is just better to wipe it out.
There was a problem hiding this comment.
Maybe should we deprecate it first? In any case, that should probably happen in another PR.
|
@gares CI green |
Some users are complaining that loading elpi loads part of the stdlib with many axioms even if they are not using them.
This PR tries to improve on that point.