diff options
Diffstat (limited to 'test-suite/success/bteauto.v')
| -rw-r--r-- | test-suite/success/bteauto.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 730b367d60..cea7d92c0b 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -149,10 +149,10 @@ Module IterativeDeepening. Class B. Class C. - Instance: B -> A | 0. - Instance: C -> A | 0. - Instance: C -> B -> A | 0. - Instance: A -> A | 0. + Instance: B -> A | 0 := {}. + Instance: C -> A | 0 := {}. + Instance: C -> B -> A | 0 := {}. + Instance: A -> A | 0 := {}. Goal C -> A. intros. |