Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given.

This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.

By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.

See penultimate commit for discussion.

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index e388acdcb0..8fad41cd8f 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -101,3 +101,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
         | F  => f y H1
         | G _ => f y H2
         end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+   no explicit type constraint is given (and when the
+   "inversion-and-dependencies-as-evars" strategy is not strong enough
+   because of a constructor with a type whose pattern structure is not
+   refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+        match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end.