diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Wf.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 9b7ea04748..c4d06fd722 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -27,7 +27,7 @@ Section Well_founded. Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := + Fixpoint Fix_F_sub (x : A) (r : Acc R x) : P x := F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) (Acc_inv r (proj2_sig y))). |