aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/CasesDep.v4
1 files changed, 2 insertions, 2 deletions
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.