From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/success/ImplicitArguments.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'test-suite/success/ImplicitArguments.v') diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index f702aa62..921433ca 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -21,3 +21,14 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A (* Test sharing information between different hypotheses *) Parameters (a:_) (b:a=0). + +(* These examples were failing due to a lifting wrongly taking let-in into account *) + +Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl. + +Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat. + +(* Some example which should succeed with local implicit arguments *) + +Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A. +Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P. -- cgit v1.2.3