From ab2ce9241e989ac899e4d43333b527e124c0c749 Mon Sep 17 00:00:00 2001
From: JPR
Date: Thu, 23 May 2019 23:44:32 +0200
Subject: Fixing typos - Part 3

---
 pretyping/evarsolve.ml        | 4 ++--
 test-suite/success/CasesDep.v | 4 ++--
 theories/Reals/RIneq.v        | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 0925215b1c..c8b1c62db0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -284,9 +284,9 @@ let noccur_evar env evd evk c =
   in
   try occur_rec false (0,env) c; true with Occur -> false
 
-(***************************************)
+(****************************************)
 (* Managing chains of local definitions *)
-(***************************************)
+(****************************************)
 
 type alias =
 | RelAlias of int
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index b0398ca056..02e15b8ee2 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -62,7 +62,7 @@ Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option n
 
 (* -------------------------------------------------------------------- *)
 (*   Example to test patterns matching on dependent families            *)
-(* This exemple extracted from the development done by Nacira Chabane  *)
+(* This exemple extracted from the development done by Nacira Chabane   *)
 (* (equipe Paris 6)                                                     *)
 (* -------------------------------------------------------------------- *)
 
@@ -298,7 +298,7 @@ End Version1.
 
 
 (* ------------------------------------------------------------------*)
-(*          Initial exemple (without patterns)                       *)
+(*          Initial example (without patterns)                       *)
 (*-------------------------------------------------------------------*)
 
 Module Version2.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index c41ab905e0..45cd74cf48 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -95,7 +95,7 @@ Proof.
 Qed.
 
 (*********************************************************)
-(** ** Relating [<], [>], [<=] and [>=]  	         *)
+(** ** Relating [<], [>], [<=] and [>=]                  *)
 (*********************************************************)
 
 (*********************************************************)
@@ -711,7 +711,7 @@ Proof.
 Qed.
 
 (*********************************************************)
-(** ** Subtraction                                      *)
+(** ** Subtraction                                       *)
 (*********************************************************)
 
 Lemma Rminus_0_r : forall r, r - 0 = r.
@@ -1352,7 +1352,7 @@ Proof.
 Qed.
 
 (*********************************************************)
-(** ** Order and subtraction                            *)
+(** ** Order and subtraction                             *)
 (*********************************************************)
 
 Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0.
-- 
cgit v1.2.3