The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/30/2016 11:38 PM, Jason Gross wrote:
> It wasn't previously in my toolbox, but now it's on my radar.
>
> I wonder what happens if you use [abstract] in the implicit tactic...  I
> wonder if you can make it loop by getting it to be called recursively from
> inside the implicit tactic...  I wonder what happens if you're in universe
> polymorphic mode and you generate new universes that show up only in
> constraints and not in the proof term...

I just wonder if someone will ever fix it ;-)  It looks like it has been 
broken for a long time - some googling suggests maybe since 8.2?  It was 
put in in 8.1, according to CHANGES.

It would also be nice if/when it works if it didn't require complete 
solution or shelving - that way it could just transform implicit goals, 
or decide to do nothing, and leave the goal go wherever it would 
otherwise normally go - on the shelf, as a focused subgoal, etc.  Also, 
that way "Declare Implicit Tactic idtac" would return behavior to the 
default.

-- Jonathan

> On Thu, Jun 30, 2016, 7:29 PM Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
>
> > On 06/30/2016 04:00 PM, Jonathan Leivent wrote:
> > > ...
> > >
> > > Hint Extern 0 (eq _ _) => typeclasses eauto : tcinit_db.
> > >
> > > Declare Implicit Tactic (eauto with nocore tcinit_db; shelve).
> > >
> > > Yes, that could be a winner.
> > >
> > > Although now it looks like Declare Implicit Tactic has some bugs. The
> > > declared tactic doesn't get called in all the cases it claims: "It is
> > > used every time the term argument of a tactic has one of its holes not
> > > fully resolved.".  For instance, "refine _" doesn't call it.
> > >
> > > And in one case, it is giving me: "Anomaly: Evar ?X96 was not
> > > declared. Please report."
> > On second thought - it seems easier to get Declare Implicit Tactic to
> > fail than to succeed.  I guess nobody uses it.
> >
> >
> > -- Jonathan