Imported Upstream version 8.5~beta1+dfsg

1 files changed, 31 insertions, 0 deletions

diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index b6337586..4116a5eb 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -5,6 +5,11 @@ Inductive t : Set :=
 
 Print t_rect.
 
+Record TT : Type := CTT { f1 := 0 : nat; f2: nat; f3 : f1=f1 }.
+
+Eval cbv in fun d:TT => match d return 0 = 0 with CTT a _ b => b end.
+Eval lazy in fun d:TT => match d return 0 = 0 with CTT a _ b => b end.
+
 (* Do not contract nested patterns with dependent return type *)
 (* see bug #1699 *)
 
@@ -34,6 +39,18 @@ Fixpoint foo (A:Type) (l:list A) : option A :=
 
 Print foo.
 
+(* Accept and use notation with binded parameters *)
+
+Inductive I (A: Type) : Type := C : A -> I A.
+Notation "x <: T" := (C T x) (at level 38).
+
+Definition uncast A (x : I A) :=
+match x with
+ | x <: _ => x
+end.
+
+Print uncast.
+
 (* Do not duplicate the matched term *)
 
 Axiom A : nat -> bool.
@@ -46,3 +63,17 @@ Definition foo' :=
 
 Print foo'.
 
+(* Was bug #3293 (eta-expansion at "match" printing time was failing because
+   of let-in's interpreted as being part of the expansion)  *)
+
+Variable b : bool.
+Variable P : bool -> Prop.
+Inductive B : Prop := AC : P b -> B.
+Definition f : B -> True.
+
+Proof.
+intros [].
+destruct b as [|] ; intros _ ; exact Logic.I.
+Defined.
+
+Print f.