From 177f7fa97dc7a2c4459f1a1047dec801ff0c65c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Nov 2018 04:18:36 +0100
Subject: [options] Remove deprecated option automatic introduction.

---
 test-suite/bugs/closed/bug_2001.v | 4 +---
 test-suite/bugs/closed/bug_6661.v | 2 --
 2 files changed, 1 insertion(+), 5 deletions(-)

(limited to 'test-suite/bugs')

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.
-- 
cgit v1.2.3