Merge PR #262: A cleaning step in using heuristics for inference of the return clause

2 files changed, 41 insertions, 8 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index dfab400baa..cb835ab48d 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -64,14 +64,9 @@ In environment
 texpDenote : forall t : type, texp t -> typeDenote t
 t : type
 e : texp t
-t1 : type
-t2 : type
-t0 : type
-b : tbinop t1 t2 t0
-e1 : texp t1
-e2 : texp t2
-The term "0" has type "nat" while it is expected to have type
- "typeDenote t0".
+n : nat
+The term "n" has type "nat" while it is expected to have type
+ "typeDenote ?t@{t1:=Nat}".
 fun '{{n, m, _}} => n + m
      : J -> nat
 fun '{{n, m, p}} => n + m + p
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..356a67efec 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,41 @@ 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.
+
+(* 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.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+   variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end).
+Qed.