aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_3495.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v
index 7b0883f910..47db64a096 100644
--- a/test-suite/bugs/closed/bug_3495.v
+++ b/test-suite/bugs/closed/bug_3495.v
@@ -1,7 +1,7 @@
Require Import RelationClasses.
Axiom R : Prop -> Prop -> Prop.
-Declare Instance : Reflexive R.
+Declare Instance R_refl : Reflexive R.
Class bar := { x : False }.
Record foo := { a : Prop ; b : bar }.