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.

0 files changed, 0 insertions, 0 deletions