diff options
| -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 ee9f8edfd3..d6c31c6b41 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 feff8af2a5..ae212caa5d 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 |