From c5e2f573ef079800eed4c8246c4f2bd39bf47b26 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 19 Jan 2019 18:20:36 -0800
Subject: Apply implicit binders to Hypothesis inside sections.

---
 test-suite/bugs/closed/bug_9363.v        | 17 +++++++++++++++++
 test-suite/success/AdvancedTypeClasses.v |  2 +-
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_9363.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_9363.v b/test-suite/bugs/closed/bug_9363.v
new file mode 100644
index 0000000000..a3f6ad9fa2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9363.v
@@ -0,0 +1,17 @@
+(* Outside a section, Hypothesis, Variable, Axiom all obey implicit binders *)
+Hypothesis foo1 : forall {n : nat}, True.
+Variable foo1' : forall {n : nat}, True.
+Axiom foo1'' : forall {n : nat}, True.
+Check foo1 (n := 1).
+Check foo1' (n := 1).
+Check foo1'' (n := 1).
+
+Section bar.
+(* Inside a section, Hypothesis and Variable do not, but they should *)
+Hypothesis foo2 : forall {n : nat}, True.
+Variable foo2' : forall {n : nat}, True.
+Axiom foo2'' : forall {n : nat}, True.
+Check foo2 (n := 1).
+Check foo2' (n := 1).
+Check foo2'' (n := 1).
+End bar.
diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
index d0aa5c8578..0253ec46e4 100644
--- a/test-suite/success/AdvancedTypeClasses.v
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -71,7 +71,7 @@ Variable Inhabited: term -> Prop.
 Variable Inhabited_correct: forall `{interp_pair p}, Inhabited (repr p) -> p.
 
 Lemma L : Prop * A -> bool * (Type -> Set) .
-apply (Inhabited_correct _ _).
+apply Inhabited_correct.
 change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))).
 Admitted.
 
-- 
cgit v1.2.3