From 2422aeb2b59229891508f35890653a9737988c00 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 Aug 2016 16:52:12 +0200
Subject: Trying a no-inversion no-dependency heuristic for match return
 clause.

The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.

See previous commit for discussion.
---
 test-suite/success/Case13.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..e388acdcb0 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,17 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a 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) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+        match y with
+        | F  => f y H1
+        | G _ => f y H2
+        end : Q y z.
-- 
cgit v1.2.3