diff options
| author | JPR | 2019-05-23 23:44:32 +0200 |
|---|---|---|
| committer | JPR | 2019-05-23 23:44:32 +0200 |
| commit | ab2ce9241e989ac899e4d43333b527e124c0c749 (patch) | |
| tree | 60ff7a9d9530b47a1bcff8db86b87b04fe6e7846 | |
| parent | d306f5428db0d034aea55d3f0699c67c1f296cc1 (diff) | |
Fixing typos - Part 3
| -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. |