diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2117.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2117.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v index 763d85e2c..6377a8b74 100644 --- a/test-suite/bugs/closed/shouldsucceed/2117.v +++ b/test-suite/bugs/closed/shouldsucceed/2117.v @@ -44,7 +44,7 @@ Ltac Subst := apply substcopy;intros;EtaLong. Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A). Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A. -Theorem church0: forall i:Type, exists X:(i->i)->i->i, +Theorem church0: forall i:Type, exists X:(i->i)->i->i, copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)). intros. esplit. |