The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 08/01/2013 07:30 PM, 
rpgcbaptista AT gmail.com
 wrote:
> Axiom OJQZ : forall {i1}, 0 = + i1<->  False.
>
> [...]
>
>    rw_aux OJQZ. (*<- This fails *)
>
>    progress repeat
>    match goal with
>    | [H1 : _ |- _] =>  progress (
>      apply (proj1 OJQZ) in H1 ||
>      (apply eq_sym in H1; apply (proj1 OJQZ) in H1; try apply eq_sym in H1))
>    | [|- _] =>  progress (
>      apply (proj2 OJQZ) ||
>      (apply eq_sym; apply (proj2 OJQZ); try apply eq_sym))
>    end. (*<- This works even though it's just the body of rw_aux *)
>    

Could this be because of the implicit argument of [OJQZ]?  The extra 
context provided by, e.g., the immediate use of [proj1] and [proj2] 
might be helping type inference work.