The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

Hello

Not sure whether the list is the right place to put it, since I'm
reasonably sure this is a bug.

Consider the following code (* and behavior *):


Hypothesis IMP : forall P Q : Prop,  (P -> Q) = (~ P \/ Q).
(** can of course be proven using classic and propositional
extensionality *)

Hint Rewrite IMP : elim_connectives.

Lemma L1 : forall X (f g : X -> X -> X -> Prop) , f = f. 
  intros.
  autorewrite with elim_connectives in *.
  (* autorewrite rewrites IMP in g but not in f, 
     leaving an ill typed g *)
  reflexivity. (* Here I get "Proof completed" *)
Qed. (* Fails with a typing error *)


This behavior raises 2 questions:

1. Why does autorewrite rewrite in g although the lemma does not apply
2. Why doesn't it rewrite in f, which has the same type (but occurs in
the goal)


-- 
Regards
Christian