diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-17 18:11:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-17 18:35:27 +0100 |
| commit | 65b901534649c5f29e245a4960fa66f6e9d9c257 (patch) | |
| tree | 0acde205596fad22223998e90e6beccf433c0263 /test-suite/bugs/closed/4574.v | |
| parent | f46a5686853353f8de733ae7fbd21a3a61977bc7 (diff) | |
Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
The setoid_rewrite tactic was not checking that the relation it was looking for
was indeed a relation, i.e. that its type was an arity.
Diffstat (limited to 'test-suite/bugs/closed/4574.v')
| -rw-r--r-- | test-suite/bugs/closed/4574.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4574.v b/test-suite/bugs/closed/4574.v new file mode 100644 index 000000000..39ba19036 --- /dev/null +++ b/test-suite/bugs/closed/4574.v @@ -0,0 +1,8 @@ +Require Import Setoid. + +Definition block A (a : A) := a. + +Goal forall A (a : A), block Type nat. +Proof. +Fail reflexivity. + |