diff options
| -rw-r--r-- | theories/NArith/BinPos.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 8123d8d85e..dc6156d6a7 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -578,7 +578,7 @@ trivial. Qed. Theorem Prect_base : forall (P:positive->Type) (a:P xH) - (f:forall p, P p -> P (Psucc p)) (p:positive), Prect P a f xH = a. + (f:forall p, P p -> P (Psucc p)), Prect P a f xH = a. Proof. trivial. Qed. |