diff options
Diffstat (limited to 'test-suite/success/ImplicitArguments.v')
| -rw-r--r-- | test-suite/success/ImplicitArguments.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index f702aa62f..f07773f8b 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -21,3 +21,9 @@ 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. |