diff options
author | 2014-08-18 18:42:11 +0200 | |
---|---|---|
committer | 2014-08-18 18:42:11 +0200 | |
commit | c54b186ecef5c71604b9b57acef278a0d09a4096 (patch) | |
tree | 7992ac889a38b7076647168f09c3c6039d3b0e3c | |
parent | 8d5238f09a6d7e0b8cb64a21d5d1410c519ff1ab (diff) |
Fix test-suite files.
-rw-r--r-- | test-suite/bugs/closed/3310.v | 5 | ||||
-rw-r--r-- | test-suite/bugs/closed/3387.v | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/3310.v b/test-suite/bugs/closed/3310.v index ee9f8edfd..d6c31c6b4 100644 --- a/test-suite/bugs/closed/3310.v +++ b/test-suite/bugs/closed/3310.v @@ -1,10 +1,11 @@ Set Primitive Projections. +Set Implicit Arguments. CoInductive stream A := cons { hd : A; tl : stream A }. -CoFixpoint id {A} (s : stream A) := cons _ (hd s) (id (tl s)). +CoFixpoint id {A} (s : stream A) := cons (hd s) (id (tl s)). Lemma id_spec : forall A (s : stream A), id s = s. Proof. intros A s. -Fail Timeout 1 change (id s) with (cons _ (hd (id s)) (tl (id s))). +Fail change (id s) with (cons (hd (id s)) (tl (id s))). diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v index feff8af2a..ae212caa5 100644 --- a/test-suite/bugs/closed/3387.v +++ b/test-suite/bugs/closed/3387.v @@ -16,6 +16,6 @@ Proof. let x := constr:(Type) in let y := constr:(Obj set_cat) in first [ unify x y | fail 2 "no unify" ]; - change x with y. (* Error: Not convertible. *) + change x with y at -1. (* Error: Not convertible. *) reflexivity. Defined.
\ No newline at end of file |