aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1905.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1939.v2
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v
index bd7fd79672..fb2725c976 100644
--- a/test-suite/bugs/closed/shouldsucceed/1905.v
+++ b/test-suite/bugs/closed/shouldsucceed/1905.v
@@ -1,5 +1,5 @@
-Require Import Setoid.
+Require Import Setoid Program.
Axiom t : Set.
Axiom In : nat -> t -> Prop.
diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/shouldsucceed/1939.v
index 0399b11241..3aa55e834c 100644
--- a/test-suite/bugs/closed/shouldsucceed/1939.v
+++ b/test-suite/bugs/closed/shouldsucceed/1939.v
@@ -1,4 +1,4 @@
-Require Import Setoid.
+Require Import Setoid Program.Basics.
Parameter P : nat -> Prop.
Parameter R : nat -> nat -> Prop.