← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/success/Case13.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/success/Case13.v
 
1
(* Check coercions in patterns *)
 
2
 
 
3
Inductive I : Set :=
 
4
  | C1 : nat -> I
 
5
  | C2 : I -> I.
 
6
 
 
7
Coercion C1 : nat >-> I.
 
8
 
 
9
(* Coercion at the root of pattern *)
 
10
Check (fun x => match x with
 
11
                | C2 n => 0
 
12
                | O => 0
 
13
                | S n => n
 
14
                end).
 
15
 
 
16
(* Coercion not at the root of pattern *)
 
17
Check (fun x => match x with
 
18
                | C2 O => 0
 
19
                | _ => 0
 
20
                end).
 
21
 
 
22
(* Unification and coercions inside patterns *)
 
23
Check
 
24
  (fun x : option nat => match x with
 
25
                         | None => 0
 
26
                         | Some O => 0
 
27
                         | _ => 0
 
28
                         end).
 
29
 
 
30
(* Coercion up to delta-conversion, and unification *)
 
31
Coercion somenat := Some (A:=nat).
 
32
Check (fun x => match x with
 
33
                | None => 0
 
34
                | O => 0
 
35
                | S n => n
 
36
                end).
 
37
 
 
38
(* Coercions with parameters *)
 
39
Inductive listn : nat -> Set :=
 
40
  | niln : listn 0
 
41
  | consn : forall n : nat, nat -> listn n -> listn (S n).
 
42
 
 
43
Inductive I' : nat -> Set :=
 
44
  | C1' : forall n : nat, listn n -> I' n
 
45
  | C2' : forall n : nat, I' n -> I' n.
 
46
 
 
47
Coercion C1' : listn >-> I'.
 
48
Check (fun x : I' 0 => match x with
 
49
                       | C2' _ _ => 0
 
50
                       | niln => 0
 
51
                       | _ => 0
 
52
                       end).
 
53
Check (fun x : I' 0 => match x with
 
54
                       | C2' _ niln => 0
 
55
                       | _ => 0
 
56
                       end).
 
57
 
 
58
(* Check insertion of coercions around matched subterm *)
 
59
 
 
60
Parameter A:Set.
 
61
Parameter f:> A -> nat.
 
62
 
 
63
Inductive J : Set := D : A -> J.
 
64
 
 
65
Check (fun x => match x with
 
66
                | D 0 => 0
 
67
                | D _ => 1
 
68
                end).
 
69
 
 
70
(* Check coercions against the type of the term to match *)
 
71
(* Used to fail in V8.1beta *)
 
72
 
 
73
Inductive C : Set := c : C.
 
74
Inductive E : Set := e :> C -> E.
 
75
Check fun (x : E) => match x with c => e c end.
 
76
 
 
77
(* Check coercions with uniform parameters (cf bug #1168) *)
 
78
 
 
79
Inductive C' : bool -> Set := c' : C' true.
 
80
Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 
81
Check fun (x : E' true) => match x with c' => e' true c' end.