Merge branch 'experimental/upstream' into upstream

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 203fbbb7..da5dd5e4 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -54,6 +54,15 @@ Check
    | Build_B x0 x1 => f x0 x1
    end).
 
+(* Check inductive types with local definitions (constructors) *)
+
+Inductive I1 : Set := C1 (_:I1) (_:=0).
+
+Check (fun x:I1 =>
+  match x with
+  | C1 i n => (i,n)
+  end).
+
 (* Check implicit parameters of inductive types (submitted by Pierre
   Casteran and also implicit in #338) *)
 
@@ -78,3 +87,23 @@ Record P:Type := {PA:Set; PB:Set}.
 Definition F (p:P) := (PA p) -> (PB p).
 
 Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F.
+
+(* Check that test for binders capturing implicit arguments is not stronger
+   than needed (problem raised by Cedric Auger) *)
+
+Set Implicit Arguments.
+Inductive bool_comp2 (b: bool): bool -> Prop :=
+| Opp2: forall q, (match b return Prop with
+                  | true => match q return Prop with 
+                              true => False |
+                              false => True end
+                  | false => match q return Prop with
+                              true => True |
+                              false => False end end) -> bool_comp2 b q.
+
+(* This one is still to be made acceptable...
+
+Set Implicit Arguments.
+Inductive I A : A->Prop := C a : (forall A, A) -> I a.
+
+ *)