From 0ad26633a4589d77de1f864733d1d953dab9ea91 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 19 Nov 2017 22:53:28 +0100
Subject: Fix (partial) #4878: option to stop autodeclaring axiom as instance.

---
 test-suite/bugs/closed/3559.v         | 1 +
 test-suite/bugs/closed/HoTT_coq_064.v | 1 +
 2 files changed, 2 insertions(+)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index da12b68689..5210b27032 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -65,6 +65,7 @@ Axiom path_iff_hprop_uncurried : forall `{IsHProp A, IsHProp B}, (A <-> B) -> A
 = B.
 Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V.
 Axiom is0trunc_V : IsTrunc (trunc_S (trunc_S minus_two)) V.
+Existing Instance is0trunc_V.
 Axiom bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}.
 Axiom bisimulation_refl : forall (v : V), bisimulation v v.
 Axiom bisimulation_eq : forall (u v : V), bisimulation u v -> u = v.
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
index b4c745375f..d02a5f120c 100644
--- a/test-suite/bugs/closed/HoTT_coq_064.v
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -178,6 +178,7 @@ Definition IsColimit `{Funext} C D (F : Functor D C)
 
 Generalizable All Variables.
 Axiom fs : Funext.
+Existing Instance fs.
 
 Section bar.
 
-- 
cgit v1.2.3