Extend the computation of dependencies in pattern-matching compilation

to the dependencies in the real arguments (a.k.a. indices) of the
terms to match.

This allows in particular to make the example from bug report #2404
work.

TODO: move the computation of dependencies in compile_branch at the time
of splitting a branch (where the computation is done now, it does not allow
to support dependent matching on the second argument of a constructor of
type  "forall b, (if b then Vector.t n else nat) -> Vector.t n -> foo").

TODO: take dependencies in Var's into account and take dependencies within
non-Rel arguments also into account (as in "match v (f t) with ... end"
where v is a Var and the type of (f t) depends on it).

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

0 files changed, 0 insertions, 0 deletions