aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith/Ndist.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/NArith/Ndist.v')
-rw-r--r--theories/NArith/Ndist.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v
index 9d399f5cd..22adc5050 100644
--- a/theories/NArith/Ndist.v
+++ b/theories/NArith/Ndist.v
@@ -333,4 +333,4 @@ Proof.
intro. rewrite <- H. apply Nplength_ultra.
rewrite Nxor_assoc. rewrite <- (Nxor_assoc a'' a'' a'). rewrite Nxor_nilpotent.
rewrite Nxor_neutral_left. reflexivity.
-Qed. \ No newline at end of file
+Qed.