From 5c30cf26474aa4f52d26005c797130a0d6d21ab5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 May 2017 18:23:05 +0200
Subject: Fixing a failure to interpret some local implicit arguments in
 Inductive.

For instance, the following was failing to use the implicitness of n:

Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
---
 test-suite/success/ImplicitArguments.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f07773f8bd..921433cadd 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -27,3 +27,8 @@ Parameters (a:_) (b:a=0).
 Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
 
 Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
+
+(* Some example which should succeed with local implicit arguments *)
+
+Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
+Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.
-- 
cgit v1.2.3