diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1634.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1634.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v index e0c540f3..0150c250 100644 --- a/test-suite/bugs/closed/shouldsucceed/1634.v +++ b/test-suite/bugs/closed/shouldsucceed/1634.v @@ -18,7 +18,7 @@ Add Parametric Relation a : (S a) Seq Goal forall (a : A) (x y : S a), Seq x y -> Seq x y. intros a x y H. - setoid_replace x with y. + setoid_replace x with y. reflexivity. trivial. Qed. |