The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Is the following supposed to work?

Inductive foo : nat -> Prop :=
| Foo1 : foo 1
| Foo2 : foo 2.

Hint Extern 5 (foo _) => econstructor.

Inductive bar : Type :=
| Bar{n}(f : foo n)(neq : n = 2) : bar.

Hint Constructors bar.

Goal bar.
solve [eauto]. (*needs to backtrack with evar n to try Foo1 then Foo2*)
Qed.

If the extern hint for foo is replaced with "Hint Constructors foo", 
then it works (for both n=1 and n=2).  But I can't replicate that 
backtracking behavior with an extern hint - which I sometimes need to 
get finer control over which constructors are used when and at what 
cost.  Note that it also doesn't work with "Hint Extern 5 (foo _) => 
(econstructor 1 + econstructor 2), but of course does if the two 
constructors are reversed (since no backtracking is needed then).

The behavior is the same with "typeclasses eauto with core" vs. "solve 
[eauto]".

However, "solve [econstructor;[econstructor|eauto]]." solves the bar 
goal - so the backtracking I'm looking for appears to be working 
sometimes, but not in extern hints.

Is this a bug, a feature, or not fully developed?

I'm working in a recent trunk (ea57f83dfdb3738e933b33f0a919e06a80bad151, 
pulled Oct 7).

-- Jonathan