summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1416.v
blob: da67d9b04fb0a09338de21ab148e4bce9911a894 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
Set Implicit Arguments.

Record Place (Env A: Type) : Type := {
  read: Env -> A ;
  write: Env -> A -> Env ;
  write_read: forall (e:Env), (write e (read e))=e
}.

Hint Rewrite -> write_read: placeeq.

Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type :=
 {
   mkEnv: A -> B -> Env ;
   mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x)
 }.

(* when the following line is commented, the bug does not appear *)
Hint Rewrite -> mkEnv2writeL: placeeq.

Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
  (exists e1:Env, e=(write p e1 (read p e))).
Proof.
  intros Env A e p; eapply ex_intro.
  autorewrite with placeeq. (* Here is the bug *)
  auto.
Qed.