Generalize DeclareScheme to use GlobRef instead of inductive#21811
Generalize DeclareScheme to use GlobRef instead of inductive#21811thomas-lamiaux wants to merge 1 commit intorocq-prover:masterfrom
Conversation
coqbot-app
bot
added
the
needs: full CI
thomas-lamiaux
force-pushed
the
genScheme
branch
from
9c43bec to
f2eefdf
Compare
|
@coqbot run full-ci |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
| declare_object @@ object_with_locality "SCHEME" | ||
| ~cache:cache_scheme | ||
| ~subst:(Some subst_scheme) | ||
| ~discharge:(fun x -> x) |
There was a problem hiding this comment.
You should do something special for VarRef as they may vanish from the environment at section closure time depending on the segment they're defined in.
There was a problem hiding this comment.
I asked how to generalize it, I was told put GlobRef everywhere.
If you prefer another change, I need to be told exactly what you want.
There was a problem hiding this comment.
This is unrelated to my point. Putting GlobRef.t is the way to go but it doesn't preclude having to fix some bits. Here, the discharge function must be fixed.
coqbot-app
bot
added
the
needs: full CI
|
After getting roasted I implemented this fix, it is satisfactory @ppedrot ? Do I need to modify the refman ? |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
vernac/vernacexpr.mli
Outdated
| | RegisterInline | ||
| | RegisterCoqlib of qualid | ||
| | RegisterScheme of { inductive : qualid; scheme_kind : qualid } | ||
| | RegisterScheme of { key_ref : qualid; scheme_kind : qualid } |
There was a problem hiding this comment.
This is a very weird field name, I'd rather have globref or just ref to keep within the style of the rest of the code. (Also, you're not the one to have introduced it but I find that the nested record is not very useful here.)
There was a problem hiding this comment.
I have fixed it. What don't you like about the record ? It seems to me like a better practice than having RegisterScheme of qualid * qualid
There was a problem hiding this comment.
You're not wrong, but in a not so old past, having non-unique field names was a recipe for disaster so I guess I'm just overreacting to inline records.
|
Probably need rebase since #20987 was merged |
thomas-lamiaux
force-pushed
the
genScheme
branch
from
831d50e to
11efe82
Compare
coqbot-app
bot
added
the
needs: full CI
prevent registering scheme for section variables without the local attribute
thomas-lamiaux
force-pushed
the
genScheme
branch
from
11efe82 to
5013cd9
Compare
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
3 participants
First step to support #21801
make doc_gram_rsts.LPCIC/coq-elpi#986