diff options
| author | Emilio Jesus Gallego Arias | 2018-11-15 04:18:36 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-18 17:17:29 +0100 |
| commit | 177f7fa97dc7a2c4459f1a1047dec801ff0c65c0 (patch) | |
| tree | 6131bedbfc1176d14fdf2919913d703e0ba067e1 /test-suite/success | |
| parent | 25e989019f72bd435d84a1d495c7de25165556dd (diff) | |
[options] Remove deprecated option automatic introduction.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Fixpoint.v | 2 | ||||
| -rw-r--r-- | test-suite/success/autointros.v | 2 |
2 files changed, 0 insertions, 4 deletions
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) |