diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-28 13:19:47 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-28 13:39:08 +0100 |
commit | db2c6f0054d3e05f82da7494ce790c04b1976401 (patch) | |
tree | dfd0493ae6a0a13f9091aeaf4fc20b70ffa42dc9 /test-suite | |
parent | 20fe4afb53e2b68ffb06a5504a444e536d4b813e (diff) |
Fixing bug #4596: [rewrite] broke in the past few weeks.
Checking that a term was indeed a relation was made too early, as the
decomposition function recognized relations of the form "f (g .. (h x y))
with f, g unary and only h binary. We postpone this check to the very end.
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/4596.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4596.v b/test-suite/bugs/closed/4596.v new file mode 100644 index 000000000..592fdb658 --- /dev/null +++ b/test-suite/bugs/closed/4596.v @@ -0,0 +1,14 @@ +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. + +Definition T (x : bool) := x = true. + +Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat) + (s : forall n : nat, bool) + (s0 s1 : nat -> S -> S), + (forall (str0 : S) (n m : nat), + (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) -> + T (b str0 m)) -> + T (b str p). +Proof. +intros ???????? H0. +rewrite H0. |