diff options
Diffstat (limited to 'test-suite/bugs/opened/shouldnotfail/1416.v')
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1416.v | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/opened/shouldnotfail/1416.v deleted file mode 100644 index c6f4302d..00000000 --- a/test-suite/bugs/opened/shouldnotfail/1416.v +++ /dev/null @@ -1,27 +0,0 @@ -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. - |