Instead of relying on a trick to make the constructor tactic parse, put

all the tactics using the constructor keyword in one entry. This has the
side-effect to also remove the other variant of constructor from the AST.

I also needed to hack around the "tauto" tactic to make it work, by
calling directly the ML tactic through a TacExtend node. This may be
generalized to get rid of the intermingled dependencies between this
tactic and the infamous Ltac quotation mechanism.

0 files changed, 0 insertions, 0 deletions