I guess Adam is talking about the following thread:

http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/5469

IMHO, the tactic I posted to coq-club escapes the scope of patch level releases, so my initial answer would be to wait for next (>= 8.4) version.

However, since there is an apparent regression with 8.2, I'd agree to commit it in the v8.3 branch (under "popular pressure"). I don't know exactly how Adam was detecting evars before, but Gregory's proposition is obviously a hack and should never have been, in my opinion, relied on in the first place.

I'm waiting for opinions from other Coq developers (and users) before proceeding...

You can see the precise tactic I'm using in this tarball:
  http://adam.chlipala.net/dist/bedrock-20101027.tgz

It's the last definition in src/PropXTac.v.  Here's the code:

====================================
Ltac ensureNotUnif E :=
  match E with
    | E => idtac
    | ?f _ => ensureNotUnif f
    | ?f _ _ => ensureNotUnif f
    | ?f _ _ _ => ensureNotUnif f
    | ?f _ _ _ _ => ensureNotUnif f
  end.
====================================

I use the tactic in src/Separation.v, to prevent overeager unification in a tactic for crossing out matching conjuncts on both sides of an implication.

Like Adam, I would be blocked from migrating to v8.3 until this issue is resolved. I suggest providing a function 'is_evar' and a function 'contains_evar' to test where are the evars. By the way, a direct access to the function 'unify' from Ltac would be very useful to. 

Many Thanks, Arthur.

Arthur, I'm not familiar with the function "unify", but would the following tactic accomplish what you want?  It essentially unifies two terms.

Ltac equate x y := let H := fresh "H" in assert (H : x = y) by reflexivity; clear H.

Yes, I guess 'equate' would behave like 'unify', though it would be nicer if there was a standard mechanism, to avoid every developer coming up with a trick of his own for unifying terms.
Arthur

(In reply to comment #2)
> Ltac ensureNotUnif E :=
>   match E with
>     | E => idtac
>     | ?f _ => ensureNotUnif f
>     | ?f _ _ => ensureNotUnif f
>     | ?f _ _ _ => ensureNotUnif f
>     | ?f _ _ _ _ => ensureNotUnif f
>   end.

I don't see what in Ltac documentation would guarantee the semantics of that.

(In reply to comment #4)
> Ltac equate x y := let H := fresh "H" in assert (H : x = y) by reflexivity;
> clear H.

On the other hand, this one looks fine to me (and I use similar stuff myself).

(In reply to comment #3)
> Like Adam, I would be blocked from migrating to v8.3 until this issue is
> resolved. I suggest providing a function 'is_evar' and a function
> 'contains_evar' to test where are the evars. By the way, a direct access to the
> function 'unify' from Ltac would be very useful to. 

Is 'is_evar' different from my 'match_evar'? Could you give use cases for 'is_evar' and 'contains_evar'? Maybe a new kind of pattern explicitly matching evars would be useful... but this looks too intrusive for a PL release.

> I don't see what in Ltac documentation would guarantee the semantics of that.

Yes, I found this behavior by trial and error.  However, do you really want to be taking the position that all the important behavior of Ltac be documented precisely?  I don't see a formal semantics in the manual, so this seems like a dangerous path. ;)

> Could you give use cases for 'is_evar' and 'contains_evar'?

I don't have a 'good' example in mind right now, but I remember cases where writing my tactic with 'is_evar' would have been simple but where I came up with complicated work-around to avoid using Adam's hack, precisely because I suspected that the hack of matching a term with itself would most probably end up being broken at some point. 

Let me now give one 'bad' motivation for 'contains_evar', which is the reason that would prevent me from migrating to v8.3. Currently (in v8.2 and v8.3), the semantics of "autorewrite" is such that it usually loops forever when invoked on terms that contain evars (I have sent a message on coqdev explaining why this happen and how to fix it). Currently, my tactics check that there is no evar in the goal before calling autorewrite, so that I don't end up restarting Coqide every two minutes... 

Arthur

Sorry, I forgot a point:

> "Maybe a new kind of pattern explicitly matching evars would be useful... but this looks too intrusive for a PL release."

That would be great! You only need to find one token to refer to evars. Let's say it's the token "@@evar". 

Then one could write:

"match t with @@evar => .."

as well as

"match t with context[ @@evar ] => .."

That would be perfect, I guess.

Note that the prefix @@ should not break many scripts, since building a user notation on top of the @ symbol is a pretty bad idea. Since the feature would not break many scripts and would be only a few lines of Caml to implement, I would say it's a good candidate for a PL release :)

Arthur

Sorry, I forgot a point:

> "Maybe a new kind of pattern explicitly matching evars would be useful... but this looks too intrusive for a PL release."

That would be great! You only need to find one token to refer to evars. Let's say it's the token "@@evar". 

Then one could write:

"match t with @@evar => .."

as well as

"match t with context[ @@evar ] => .."

That would be perfect, I guess.

Note that the prefix @@ should not break many scripts, since building a user notation on top of the @ symbol is a pretty bad idea. Since the feature would not break many scripts and would be only a few lines of Caml to implement, I would say it's a good candidate for a PL release :)

Arthur

(In reply to comment #7)
> [...]  However, do you really want to
> be taking the position that all the important behavior of Ltac be documented
> precisely? [...]

No, but I avoid relying on behaviours that are obviously buggy...

Anyway, as nobody gave me a more elegant way to test evars, I've committed the new tactic "is_evar" v8.3 branch (r13636). It should be part of the next PL release.

(In reply to comment #10)
> "match t with context[ @@evar ] => .."

This could be written "match t with context[ ?t ] => is_evar t; ..." with the is_evar tactic. However, be aware that context only matches closed terms.

> Note that the prefix @@ should not break many scripts, since building a user
> notation on top of the @ symbol is a pretty bad idea. Since the feature would
> not break many scripts and would be only a few lines of Caml to implement, I
> would say it's a good candidate for a PL release :)

I would like to see the few lines of Caml... :-) To me, it would mean changing the AST of patterns (but maybe I'm wrong), which is too intrusive for a PL release IMHO. It could be a new feature to be experimented in the trunk, though. Feel free to submit a new wishlist bug and/or a patch for this.

Thanks, that looks perfect!

I also added "has_evar" (which goes under binders) in the v8.3 branch (r13658).