diff options
| author | Pierre-Marie Pédrot | 2018-11-19 13:38:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:38:48 +0100 |
| commit | 6498a76f9755a9c82a04f0c4e088bc809eedede5 (patch) | |
| tree | 2db09d01926223466adfa5864573fb27960a38ea /test-suite | |
| parent | d73fee2674999225ce59cc0a9f61dfafe99d7689 (diff) | |
| parent | 177f7fa97dc7a2c4459f1a1047dec801ff0c65c0 (diff) | |
Merge PR #9001: [options] Remove deprecated option automatic introduction.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_2001.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_6661.v | 2 | ||||
| -rw-r--r-- | test-suite/success/Fixpoint.v | 2 | ||||
| -rw-r--r-- | test-suite/success/autointros.v | 2 |
4 files changed, 1 insertions, 9 deletions
diff --git a/test-suite/bugs/closed/bug_2001.v b/test-suite/bugs/closed/bug_2001.v index 652c65706a..31c62b7b36 100644 --- a/test-suite/bugs/closed/bug_2001.v +++ b/test-suite/bugs/closed/bug_2001.v @@ -1,12 +1,10 @@ (* 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. -Definition f (s:nat) (t:T) : nat. +Definition f : forall (s:nat) (t:T), nat. fix f 2. intros s t. refine diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v index e88a3704d8..28a9ffc7bd 100644 --- a/test-suite/bugs/closed/bug_6661.v +++ b/test-suite/bugs/closed/bug_6661.v @@ -53,8 +53,6 @@ Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X. exact x. Defined. -Unset Automatic Introduction. - Definition idfun (T : UU) := λ t:T, t. Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index efb32ef6f7..81c9763ccd 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -50,8 +50,6 @@ End folding. (* Check definition by tactics *) -Set Automatic Introduction. - Inductive even : nat -> Type := | even_O : even 0 | even_S : forall n, odd n -> even (S n) diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v index 0a0812711c..1140a537fc 100644 --- a/test-suite/success/autointros.v +++ b/test-suite/success/autointros.v @@ -1,5 +1,3 @@ -Set Automatic Introduction. - Inductive even : nat -> Prop := | even_0 : even 0 | even_odd : forall n, odd n -> even (S n) |