Why is tauto_plugin separate from ltac_plugin?
tauto was considered a general tactic not tied to Ltac? At least this was what I thought meant sense to say in the draft of the planned user survey.
it's mentioned in the survey?
I would say tauto is about as separate from ltac as rewrite, but rewrite is in ltac_plugin
@Gaëtan Gilbert you could ask the same question for any plugin defining tactics
actually tauto is half implemented in ltac so it's less separate than rewrite
@Karl Palmskog IMO the whole Ltac vs. "proof language" stuff is very misleading
all of this stuff are Ltac definitions / notations
I think it's a historical accident that we keep insisting so much on Ltac being the glue around the basic proof primitives
in the manual, I don't think the presentation of Micromega and "Logic/equality tactics" is fundamentally different. It's basically some magic words you use to solve goals in different contexts.
which are not basic at all, anyways
should users really (have to) care about whether some domain-specific automation is implemented in Ltac or OCaml? My assumption has been that they normally shouldn't
They shouldn't indeed. But the current discussion is mostly about OCaml code organization, so it's irrelevant for the end user
OK, still valuable to know that the tie between tauto-ltac is so tight, so if one wants to got Ltac2-only one will have to skip tauto and friends...
Last updated: Jun 09 2023 at 07:01 UTC