Declaration of multiple hypotheses or parameters now share typing

information for inference of implicit arguments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16487 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 0 deletions

diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index a654080de..f702aa62f 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -17,3 +17,7 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A
     | vnil => w
     | vcons a v' => vcons a (app v' w)
   end.
+
+(* Test sharing information between different hypotheses *)
+
+Parameters (a:_) (b:a=0).