diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/bugs/closed/shouldsucceed/846.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/846.v')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/846.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v index a963b225..ee5ec1fa 100644 --- a/test-suite/bugs/closed/shouldsucceed/846.v +++ b/test-suite/bugs/closed/shouldsucceed/846.v @@ -27,7 +27,7 @@ Definition index := list bool. Inductive L (A:Set) : index -> Set := initL: A -> L A nil - | pluslL: forall l:index, One -> L A (false::l) + | pluslL: forall l:index, One -> L A (false::l) | plusrL: forall l:index, L A l -> L A (false::l) | varL: forall l:index, L A l -> L A (true::l) | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l) @@ -109,7 +109,7 @@ Proof. exact (monL (fun x:One + A => (match (maybe (fun a:A => initL a) x) with | inl u => pluslL _ _ u - | inr t' => plusrL t' end)) r). + | inr t' => plusrL t' end)) r). Defined. Section minimal. @@ -119,11 +119,11 @@ Hypothesis G: Set -> Set. Hypothesis step: sub1 (LamF' G) G. Fixpoint L'(A:Set)(i:index){struct i} : Set := - match i with + match i with nil => A | false::l => One + L' A l | true::l => G (L' A l) - end. + end. Definition LinL': forall (A:Set)(i:index), L A i -> L' A i. Proof. @@ -177,7 +177,7 @@ Proof. assumption. induction a. simpl L' in t. - apply (aczelapp (l1:=true::nil) (l2:=i)). + apply (aczelapp (l1:=true::nil) (l2:=i)). exact (lam' IHi t). simpl L' in t. induction t. |