diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/CasesDep.v | 4 | ||||
| -rw-r--r-- | 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. |