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 /test-suite | |
| parent | d306f5428db0d034aea55d3f0699c67c1f296cc1 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/CasesDep.v | 4 |
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. |