diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1643.v | 1 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1891.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1918.v | 9 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2001.v | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v index 4114987d3..879a65b18 100644 --- a/test-suite/bugs/closed/shouldsucceed/1643.v +++ b/test-suite/bugs/closed/shouldsucceed/1643.v @@ -10,7 +10,6 @@ Definition decomp_func (s:Str) := Theorem decomp s: s = decomp_func s. Proof. - intros s. case s; simpl; reflexivity. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v index 11124cddd..2d90a2f1d 100644 --- a/test-suite/bugs/closed/shouldsucceed/1891.v +++ b/test-suite/bugs/closed/shouldsucceed/1891.v @@ -7,7 +7,7 @@ Lemma L (x: T unit): (unit -> T unit) -> unit. Proof. - refine (fun x => match x return _ with mkT n => fun g => f (g _) end). + refine (match x return _ with mkT n => fun g => f (g _) end). trivial. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v index 474ec935b..9d92fe12b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1918.v +++ b/test-suite/bugs/closed/shouldsucceed/1918.v @@ -66,14 +66,14 @@ Definition pEFct (F:k2) : Type := Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)). Proof. red. - intros X Y mX mY A B f x. + intros A B f x. exact (mX (Y A)(Y B) (mY A B f) x). Defined. (** closure under composition *) Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)). Proof. - intros X Y ef1 ef2. + intros ef1 ef2. apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp. (* prove ext *) apply (e ef1). @@ -103,7 +103,7 @@ Defined. (** closure under sums *) Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type. Proof. - intros X Y ef1 ef2. + intros ef1 ef2. set (m12:=fun (A B:Set)(f:A->B) x => match x with | inl y => inl _ (m ef1 f y) | inr y => inr _ (m ef2 f y) @@ -144,7 +144,7 @@ Defined. (** closure under products *) Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type. Proof. - intros X Y ef1 ef2. + intros ef1 ef2. set (m12:=fun (A B:Set)(f:A->B) x => match x with (x1,x2) => (m ef1 f x1, m ef2 f x2) end). apply (mkEFct(m:=m12)); red; intros. @@ -220,7 +220,6 @@ Defined. (** constants in k1 *) Lemma constEFct (C:Set): EFct (fun _ => C). Proof. - intro. set (mC:=fun A B (f:A->B)(x:C) => x). apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity. Defined. diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v index c50ad036d..d0b3bf173 100644 --- a/test-suite/bugs/closed/shouldsucceed/2001.v +++ b/test-suite/bugs/closed/shouldsucceed/2001.v @@ -1,6 +1,8 @@ (* Automatic computing of guard in "Theorem with"; check that guard is not computed when the user explicitly indicated it *) +Unset Automatic Introduction. + Inductive T : Set := | v : T. |