Pierre-Marie Pédrot
Pierre-Marie Pédrot
Even though it's unlikely to be observable in batch files, @coqbot bench
I don't think Arguments use the detyper but I may be wrong. In practice it's unlikely that outside of printing people routinely detype terms with a gazillion binders (and even...
Let's rerun CI since I tweaked the elpi overlay. @coqbot run full ci
@coqbot bench
This looks indeed like noise. Nonetheless, this patch makes it easier to further reduce the amount of typing in that function, that does keep appearing in my random profiles.
Comment added.
Having a qualified name does really entail module-scoping, we could have a reserved prefix for statically defined dbs.
For the HoTT issue, I think there is an easy local fix: we can simply statically define the global dbs that are hardcoded in the tactic implementation. From what I...
> or are syntactic "values" meant, as in the value restriction for ML? This is the intended meaning, i.e. semantically these variables are not producing any toplevel effect. > Is...
This PR will now need a rebase.