diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 3 |
2 files changed, 1 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 621a2ed9c8..adbbc5ea01 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -133,7 +133,6 @@ Proof. intros m n; unfold ltb at 1. f_equiv. rewrite recursion_succ; f_equiv'. -reflexivity. Qed. (* Above, we rewrite applications of function. Is it possible to rewrite diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 67cab5507b..f98e8da9a7 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -13,7 +13,7 @@ and proves its properties *) Require Export NSub. -Ltac f_equiv' := repeat (f_equiv; try intros ? ? ?; auto). +Ltac f_equiv' := repeat (repeat f_equiv; try intros ? ? ?; auto). Module NStrongRecProp (Import N : NAxiomsRecSig'). Include NSubProp N. @@ -82,7 +82,6 @@ Proof. intros. unfold strong_rec0. f_equiv. rewrite recursion_succ; f_equiv'. -reflexivity. Qed. Lemma strong_rec_0 : forall a, |