@Pierre-Marie Pédrot , @Emilio Jesús Gallego Arias : any objections if I move
logic.ml and similar files to
EConstr? At first view, it is only threading the
sigma (how costly could it be?) and possibly avoiding a few costly
to_constr. In particular, should I be afraid of a slowdown risk?
Beware with Logic, the other should be fine.
I remember that I had trouble with efficiency when trying to port Logic because there are a few critical calls to unsafe back and forth conversions in there
(Or maybe it was breaking? I don't remember, this was already quite a long time ago.)
But I distinctly remember porting Logic to EConstr already and not pushing it further
(Also I'd advise against wasting time on Logic. It's legacy code that is bound to disappear.)
My initial motivation was to use the API of
EConstr. I don't really care about
logic.ml, it arrives as a dependency of a change in
inductiveops.mli. So, maybe, I'll keep
logic.ml as it is then.
And is it essential that
vnorm.ml is in
Actually, I don't know how is perceived the
Inductiveops API. It avoids some inductive data routine massaging, but controlling the exact amount of job which is done is difficult.
Termops.lift_rel_context and friends are on
constr. If I need a variant of them on
EConstr, do I add them to
EConstr? Do I made a
EConstr submodule to
Termops? Any idea? (By default, I may lean to add it
Or we split
Last updated: Jun 04 2023 at 19:30 UTC