summaryrefslogtreecommitdiff
path: root/test-suite/success/Case15.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success/Case15.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success/Case15.v')
-rw-r--r--test-suite/success/Case15.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v
index 8431880d..69fca48e 100644
--- a/test-suite/success/Case15.v
+++ b/test-suite/success/Case15.v
@@ -12,7 +12,7 @@ Check
(* Suggested by Pierre Letouzey (PR#207) *)
Inductive Boite : Set :=
- boite : forall b : bool, (if b then nat else (nat * nat)%type) -> Boite.
+ boite : forall b : bool, (if b then nat else (nat * nat)%type) -> Boite.
Definition test (B : Boite) :=
match B return nat with
@@ -30,7 +30,7 @@ Check [x]
end.
Check [x]
- Cases x of
+ Cases x of
(c true true) => true
| (c false O) => true
| _ => false
@@ -40,7 +40,7 @@ Check [x]
Check
[x:I]
Cases x of
- (c b y) =>
+ (c b y) =>
(<[b:bool](if b then bool else nat)->bool>if b
then [y](if y then true else false)
else [y]Cases y of