summaryrefslogtreecommitdiff
path: root/theories/Numbers/BigNumPrelude.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/BigNumPrelude.v')
-rw-r--r--theories/Numbers/BigNumPrelude.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 45a7527c..bd893087 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -10,7 +10,7 @@
(** * BigNumPrelude *)
-(** Auxillary functions & theorems used for arbitrary precision efficient
+(** Auxiliary functions & theorems used for arbitrary precision efficient
numbers. *)
@@ -22,7 +22,7 @@ Require Export Zpow_facts.
Declare ML Module "numbers_syntax_plugin".
(* *** Nota Bene ***
- All results that were general enough has been moved in ZArith.
+ All results that were general enough have been moved in ZArith.
Only remain here specialized lemmas and compatibility elements.
(P.L. 5/11/2007).
*)