Fixing typos - Part 2

6 files changed, 8 insertions, 8 deletions

diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index e0e2232be5..7759bda7c7 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
@@ -129,7 +129,7 @@ Proof.
 intros n m H1 H2; rewrite H2 in H1; now apply H1.
 Qed.
 
-(* Propeties of plus, minus and opp *)
+(* Properties of plus, minus and opp *)
 
 Theorem Rplus_0_l : forall n : R, 0 + n == n.
 Proof.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 60931df517..c5e179fbb8 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -990,7 +990,7 @@ Proof.
   rewrite IHs. reflexivity.
 Qed.
 
-(** equality migth be (too) strong *)
+(** equality might be (too) strong *)
 Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f).
 Proof.
   destruct f.
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index bed9e55ac0..48027442b2 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1208,8 +1208,8 @@ let dump_rexpr = lazy
     
     
 (** [make_goal_of_formula depxr vars props form] where 
-     - vars is an environment for the arithmetic variables occuring in form
-     - props is an environment for the propositions occuring in form
+     - vars is an environment for the arithmetic variables occurring in form
+     - props is an environment for the propositions occurring in form
     @return a goal where all the variables and propositions of the formula are quantified
 
 *) 
@@ -1469,7 +1469,7 @@ let pre_processZ mt f =
    x <= y or (x and y are incomparable) *)
 
 (**
-  * Instanciate the current Coq goal with a Micromega formula, a varmap, and a
+  * Instantiate the current Coq goal with a Micromega formula, a varmap, and a
   * witness.
   *)
 
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 0209030b64..f038f8a71a 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -21,7 +21,7 @@ module type PHashtable =
 
     val open_in : string -> 'a t
     (** [open_in f] rebuilds a table from the records stored in file [f].
-	As marshaling is not type-safe, it migth segault.
+        As marshaling is not type-safe, it might segfault.
     *)
 
     val find : 'a t -> key -> 'a
diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli
index 4e7a388aaf..d2f3e756a9 100644
--- a/plugins/micromega/persistent_cache.mli
+++ b/plugins/micromega/persistent_cache.mli
@@ -17,7 +17,7 @@ module type PHashtable =
 
     val open_in : string -> 'a t
     (** [open_in f] rebuilds a table from the records stored in file [f].
-        As marshaling is not type-safe, it migth segault.
+        As marshaling is not type-safe, it might segfault.
     *)
 
     val find : 'a t -> key -> 'a
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index 6aebc4ca9a..e3a9f6f60f 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -200,7 +200,7 @@ let is_undefined f =
   | _ -> false;;
 
 (* ------------------------------------------------------------------------- *)
-(* Operation analagous to "map" for lists.                                   *)
+(* Operation analogous to "map" for lists.                                   *)
 (* ------------------------------------------------------------------------- *)
 
 let mapf =