← Back to branch summary

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

« back to all changes in this revision

Viewing changes to dev/ocamlweb-doc/pretyping.dep.ps

  • 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:
dev/ocamlweb-doc/pretyping.dep.ps
 
1
%!PS-Adobe-2.0
 
2
%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
 
3
%%For: (herbelin) Hugo Herbelin
 
4
%%Title: G
 
5
%%Pages: (atend)
 
6
%%BoundingBox: 35 35 577 146
 
7
%%EndComments
 
8
save
 
9
%%BeginProlog
 
10
/DotDict 200 dict def
 
11
DotDict begin
 
12
 
 
13
/setupLatin1 {
 
14
mark
 
15
/EncodingVector 256 array def
 
16
 EncodingVector 0
 
17
 
 
18
ISOLatin1Encoding 0 255 getinterval putinterval
 
19
 
 
20
EncodingVector
 
21
  dup 306 /AE
 
22
  dup 301 /Aacute
 
23
  dup 302 /Acircumflex
 
24
  dup 304 /Adieresis
 
25
  dup 300 /Agrave
 
26
  dup 305 /Aring
 
27
  dup 303 /Atilde
 
28
  dup 307 /Ccedilla
 
29
  dup 311 /Eacute
 
30
  dup 312 /Ecircumflex
 
31
  dup 313 /Edieresis
 
32
  dup 310 /Egrave
 
33
  dup 315 /Iacute
 
34
  dup 316 /Icircumflex
 
35
  dup 317 /Idieresis
 
36
  dup 314 /Igrave
 
37
  dup 334 /Udieresis
 
38
  dup 335 /Yacute
 
39
  dup 376 /thorn
 
40
  dup 337 /germandbls
 
41
  dup 341 /aacute
 
42
  dup 342 /acircumflex
 
43
  dup 344 /adieresis
 
44
  dup 346 /ae
 
45
  dup 340 /agrave
 
46
  dup 345 /aring
 
47
  dup 347 /ccedilla
 
48
  dup 351 /eacute
 
49
  dup 352 /ecircumflex
 
50
  dup 353 /edieresis
 
51
  dup 350 /egrave
 
52
  dup 355 /iacute
 
53
  dup 356 /icircumflex
 
54
  dup 357 /idieresis
 
55
  dup 354 /igrave
 
56
  dup 360 /dcroat
 
57
  dup 361 /ntilde
 
58
  dup 363 /oacute
 
59
  dup 364 /ocircumflex
 
60
  dup 366 /odieresis
 
61
  dup 362 /ograve
 
62
  dup 365 /otilde
 
63
  dup 370 /oslash
 
64
  dup 372 /uacute
 
65
  dup 373 /ucircumflex
 
66
  dup 374 /udieresis
 
67
  dup 371 /ugrave
 
68
  dup 375 /yacute
 
69
  dup 377 /ydieresis  
 
70
 
 
71
% Set up ISO Latin 1 character encoding
 
72
/starnetISO {
 
73
        dup dup findfont dup length dict begin
 
74
        { 1 index /FID ne { def }{ pop pop } ifelse
 
75
        } forall
 
76
        /Encoding EncodingVector def
 
77
        currentdict end definefont
 
78
} def
 
79
/Times-Roman starnetISO def
 
80
/Times-Italic starnetISO def
 
81
/Times-Bold starnetISO def
 
82
/Times-BoldItalic starnetISO def
 
83
/Helvetica starnetISO def
 
84
/Helvetica-Oblique starnetISO def
 
85
/Helvetica-Bold starnetISO def
 
86
/Helvetica-BoldOblique starnetISO def
 
87
/Courier starnetISO def
 
88
/Courier-Oblique starnetISO def
 
89
/Courier-Bold starnetISO def
 
90
/Courier-BoldOblique starnetISO def
 
91
cleartomark
 
92
} bind def
 
93
 
 
94
%%BeginResource: procset graphviz 0 0
 
95
/coord-font-family /Times-Roman def
 
96
/default-font-family /Times-Roman def
 
97
/coordfont coord-font-family findfont 8 scalefont def
 
98
 
 
99
/InvScaleFactor 1.0 def
 
100
/set_scale {
 
101
        dup 1 exch div /InvScaleFactor exch def
 
102
        dup scale
 
103
} bind def
 
104
 
 
105
% styles
 
106
/solid { [] 0 setdash } bind def
 
107
/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
 
108
/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
 
109
/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
 
110
/bold { 2 setlinewidth } bind def
 
111
/filled { } bind def
 
112
/unfilled { } bind def
 
113
/rounded { } bind def
 
114
/diagonals { } bind def
 
115
 
 
116
% hooks for setting color 
 
117
/nodecolor { sethsbcolor } bind def
 
118
/edgecolor { sethsbcolor } bind def
 
119
/graphcolor { sethsbcolor } bind def
 
120
/nopcolor {pop pop pop} bind def
 
121
 
 
122
/beginpage {    % i j npages
 
123
        /npages exch def
 
124
        /j exch def
 
125
        /i exch def
 
126
        /str 10 string def
 
127
        npages 1 gt {
 
128
                gsave
 
129
                        coordfont setfont
 
130
                        0 0 moveto
 
131
                        (\() show i str cvs show (,) show j str cvs show (\)) show
 
132
                grestore
 
133
        } if
 
134
} bind def
 
135
 
 
136
/set_font {
 
137
        findfont exch
 
138
        scalefont setfont
 
139
} def
 
140
 
 
141
% draw aligned label in bounding box aligned to current point
 
142
/alignedtext {                  % width adj text
 
143
        /text exch def
 
144
        /adj exch def
 
145
        /width exch def
 
146
        gsave
 
147
                width 0 gt {
 
148
                        text stringwidth pop adj mul 0 rmoveto
 
149
                } if
 
150
                [] 0 setdash
 
151
                text show
 
152
        grestore
 
153
} def
 
154
 
 
155
/boxprim {                              % xcorner ycorner xsize ysize
 
156
                4 2 roll
 
157
                moveto
 
158
                2 copy
 
159
                exch 0 rlineto
 
160
                0 exch rlineto
 
161
                pop neg 0 rlineto
 
162
                closepath
 
163
} bind def
 
164
 
 
165
/ellipse_path {
 
166
        /ry exch def
 
167
        /rx exch def
 
168
        /y exch def
 
169
        /x exch def
 
170
        matrix currentmatrix
 
171
        newpath
 
172
        x y translate
 
173
        rx ry scale
 
174
        0 0 1 0 360 arc
 
175
        setmatrix
 
176
} bind def
 
177
 
 
178
/endpage { showpage } bind def
 
179
/showpage { } def
 
180
 
 
181
/layercolorseq
 
182
        [       % layer color sequence - darkest to lightest
 
183
                [0 0 0]
 
184
                [.2 .8 .8]
 
185
                [.4 .8 .8]
 
186
                [.6 .8 .8]
 
187
                [.8 .8 .8]
 
188
        ]
 
189
def
 
190
 
 
191
/layerlen layercolorseq length def
 
192
 
 
193
/setlayer {/maxlayer exch def /curlayer exch def
 
194
        layercolorseq curlayer 1 sub layerlen mod get
 
195
        aload pop sethsbcolor
 
196
        /nodecolor {nopcolor} def
 
197
        /edgecolor {nopcolor} def
 
198
        /graphcolor {nopcolor} def
 
199
} bind def
 
200
 
 
201
/onlayer { curlayer ne {invis} if } def
 
202
 
 
203
/onlayers {
 
204
        /myupper exch def
 
205
        /mylower exch def
 
206
        curlayer mylower lt
 
207
        curlayer myupper gt
 
208
        or
 
209
        {invis} if
 
210
} def
 
211
 
 
212
/curlayer 0 def
 
213
 
 
214
%%EndResource
 
215
%%EndProlog
 
216
%%BeginSetup
 
217
14 default-font-family set_font
 
218
1 setmiterlimit
 
219
% /arrowlength 10 def
 
220
% /arrowwidth 5 def
 
221
 
 
222
% make sure pdfmark is harmless for PS-interpreters other than Distiller
 
223
/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
 
224
% make '<<' and '>>' safe on PS Level 1 devices
 
225
/languagelevel where {pop languagelevel}{1} ifelse
 
226
2 lt {
 
227
    userdict (<<) cvn ([) cvn load put
 
228
    userdict (>>) cvn ([) cvn load put
 
229
} if
 
230
 
 
231
%%EndSetup
 
232
%%Page: 1 1
 
233
%%PageBoundingBox: 36 36 577 146
 
234
%%PageOrientation: Portrait
 
235
gsave
 
236
35 35 542 111 boxprim clip newpath
 
237
36 36 translate
 
238
0 0 1 beginpage
 
239
0.3600 set_scale
 
240
0 0 translate 0 rotate
 
241
0.000 0.000 0.000 graphcolor
 
242
14.00 /Times-Roman set_font
 
243
 
 
244
%       Unification
 
245
gsave 10 dict begin
 
246
610 118 45 18 ellipse_path
 
247
stroke
 
248
gsave 10 dict begin
 
249
577 113 moveto
 
250
(Unification)
 
251
[9.6 6.96 3.84 4.8 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
 
252
xshow
 
253
end grestore
 
254
end grestore
 
255
 
 
256
%       Evarutil
 
257
gsave 10 dict begin
 
258
728 72 36 18 ellipse_path
 
259
stroke
 
260
gsave 10 dict begin
 
261
705 67 moveto
 
262
(Evarutil)
 
263
[8.4 6.72 6.24 4.8 6.96 3.84 3.84 3.84]
 
264
xshow
 
265
end grestore
 
266
end grestore
 
267
 
 
268
%       Unification -> Evarutil
 
269
newpath 643 105 moveto
 
270
657 99 674 93 689 87 curveto
 
271
stroke
 
272
gsave 10 dict begin
 
273
solid
 
274
1 setlinewidth
 
275
0.000 0.000 0.000 edgecolor
 
276
newpath 691 90 moveto
 
277
699 83 lineto
 
278
688 83 lineto
 
279
closepath
 
280
fill
 
281
0.000 0.000 0.000 edgecolor
 
282
newpath 691 90 moveto
 
283
699 83 lineto
 
284
688 83 lineto
 
285
closepath
 
286
stroke
 
287
end grestore
 
288
 
 
289
%       Pattern
 
290
gsave 10 dict begin
 
291
728 210 33 18 ellipse_path
 
292
stroke
 
293
gsave 10 dict begin
 
294
708 205 moveto
 
295
(Pattern)
 
296
[7.44 6.24 3.84 3.84 6.24 4.8 6.96]
 
297
xshow
 
298
end grestore
 
299
end grestore
 
300
 
 
301
%       Unification -> Pattern
 
302
newpath 631 134 moveto
 
303
650 150 680 173 701 189 curveto
 
304
stroke
 
305
gsave 10 dict begin
 
306
solid
 
307
1 setlinewidth
 
308
0.000 0.000 0.000 edgecolor
 
309
newpath 699 192 moveto
 
310
709 195 lineto
 
311
703 186 lineto
 
312
closepath
 
313
fill
 
314
0.000 0.000 0.000 edgecolor
 
315
newpath 699 192 moveto
 
316
709 195 lineto
 
317
703 186 lineto
 
318
closepath
 
319
stroke
 
320
end grestore
 
321
 
 
322
%       Retyping
 
323
gsave 10 dict begin
 
324
839 118 38 18 ellipse_path
 
325
stroke
 
326
gsave 10 dict begin
 
327
813 113 moveto
 
328
(Retyping)
 
329
[9.12 6 3.84 6.96 6.96 3.84 6.96 6.96]
 
330
xshow
 
331
end grestore
 
332
end grestore
 
333
 
 
334
%       Unification -> Retyping
 
335
newpath 656 118 moveto
 
336
695 118 750 118 790 118 curveto
 
337
stroke
 
338
gsave 10 dict begin
 
339
solid
 
340
1 setlinewidth
 
341
0.000 0.000 0.000 edgecolor
 
342
newpath 790 122 moveto
 
343
800 118 lineto
 
344
790 115 lineto
 
345
closepath
 
346
fill
 
347
0.000 0.000 0.000 edgecolor
 
348
newpath 790 122 moveto
 
349
800 118 lineto
 
350
790 115 lineto
 
351
closepath
 
352
stroke
 
353
end grestore
 
354
 
 
355
%       Typing
 
356
gsave 10 dict begin
 
357
839 64 32 18 ellipse_path
 
358
stroke
 
359
gsave 10 dict begin
 
360
819 59 moveto
 
361
(Typing)
 
362
[6.96 6.96 6.96 3.84 6.96 6.96]
 
363
xshow
 
364
end grestore
 
365
end grestore
 
366
 
 
367
%       Evarutil -> Typing
 
368
newpath 764 69 moveto
 
369
775 68 786 67 797 67 curveto
 
370
stroke
 
371
gsave 10 dict begin
 
372
solid
 
373
1 setlinewidth
 
374
0.000 0.000 0.000 edgecolor
 
375
newpath 797 70 moveto
 
376
807 66 lineto
 
377
797 64 lineto
 
378
closepath
 
379
fill
 
380
0.000 0.000 0.000 edgecolor
 
381
newpath 797 70 moveto
 
382
807 66 lineto
 
383
797 64 lineto
 
384
closepath
 
385
stroke
 
386
end grestore
 
387
 
 
388
%       Rawterm
 
389
gsave 10 dict begin
 
390
1109 110 39 18 ellipse_path
 
391
stroke
 
392
gsave 10 dict begin
 
393
1083 105 moveto
 
394
(Rawterm)
 
395
[9.36 5.76 10.08 3.84 6.24 4.8 10.8]
 
396
xshow
 
397
end grestore
 
398
end grestore
 
399
 
 
400
%       Pattern -> Rawterm
 
401
newpath 759 216 moveto
 
402
816 226 939 239 1024 191 curveto
 
403
1049 176 1038 155 1060 138 curveto
 
404
1069 131 1077 130 1084 129 curveto
 
405
stroke
 
406
gsave 10 dict begin
 
407
solid
 
408
1 setlinewidth
 
409
0.000 0.000 0.000 edgecolor
 
410
newpath 1085 132 moveto
 
411
1094 127 lineto
 
412
1084 126 lineto
 
413
closepath
 
414
fill
 
415
0.000 0.000 0.000 edgecolor
 
416
newpath 1085 132 moveto
 
417
1094 127 lineto
 
418
1084 126 lineto
 
419
closepath
 
420
stroke
 
421
end grestore
 
422
 
 
423
%       Inductiveops
 
424
gsave 10 dict begin
 
425
1109 164 49 18 ellipse_path
 
426
stroke
 
427
gsave 10 dict begin
 
428
1073 159 moveto
 
429
(Inductiveops)
 
430
[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24 6.96 6.96 5.52]
 
431
xshow
 
432
end grestore
 
433
end grestore
 
434
 
 
435
%       Retyping -> Inductiveops
 
436
newpath 878 120 moveto
 
437
915 122 974 126 1024 137 curveto
 
438
1037 139 1051 144 1064 148 curveto
 
439
stroke
 
440
gsave 10 dict begin
 
441
solid
 
442
1 setlinewidth
 
443
0.000 0.000 0.000 edgecolor
 
444
newpath 1063 151 moveto
 
445
1074 151 lineto
 
446
1065 145 lineto
 
447
closepath
 
448
fill
 
449
0.000 0.000 0.000 edgecolor
 
450
newpath 1063 151 moveto
 
451
1074 151 lineto
 
452
1065 145 lineto
 
453
closepath
 
454
stroke
 
455
end grestore
 
456
 
 
457
%       Pretype_errors
 
458
gsave 10 dict begin
 
459
969 72 54 18 ellipse_path
 
460
stroke
 
461
gsave 10 dict begin
 
462
927 67 moveto
 
463
(Pretype_errors)
 
464
[7.68 4.56 6 3.84 6.96 6.96 6.24 6.96 6.24 5.04 4.56 6.96 4.56 5.52]
 
465
xshow
 
466
end grestore
 
467
end grestore
 
468
 
 
469
%       Typing -> Pretype_errors
 
470
newpath 871 66 moveto
 
471
881 67 893 68 905 68 curveto
 
472
stroke
 
473
gsave 10 dict begin
 
474
solid
 
475
1 setlinewidth
 
476
0.000 0.000 0.000 edgecolor
 
477
newpath 905 71 moveto
 
478
915 69 lineto
 
479
905 65 lineto
 
480
closepath
 
481
fill
 
482
0.000 0.000 0.000 edgecolor
 
483
newpath 905 71 moveto
 
484
915 69 lineto
 
485
905 65 lineto
 
486
closepath
 
487
stroke
 
488
end grestore
 
489
 
 
490
%       Pretype_errors -> Inductiveops
 
491
newpath 998 87 moveto
 
492
1007 92 1016 98 1024 104 curveto
 
493
1042 116 1043 124 1060 137 curveto
 
494
1063 139 1067 142 1071 144 curveto
 
495
stroke
 
496
gsave 10 dict begin
 
497
solid
 
498
1 setlinewidth
 
499
0.000 0.000 0.000 edgecolor
 
500
newpath 1070 147 moveto
 
501
1080 149 lineto
 
502
1073 141 lineto
 
503
closepath
 
504
fill
 
505
0.000 0.000 0.000 edgecolor
 
506
newpath 1070 147 moveto
 
507
1080 149 lineto
 
508
1073 141 lineto
 
509
closepath
 
510
stroke
 
511
end grestore
 
512
 
 
513
%       Pretype_errors -> Rawterm
 
514
newpath 1011 84 moveto
 
515
1029 88 1048 94 1065 98 curveto
 
516
stroke
 
517
gsave 10 dict begin
 
518
solid
 
519
1 setlinewidth
 
520
0.000 0.000 0.000 edgecolor
 
521
newpath 1064 101 moveto
 
522
1075 101 lineto
 
523
1066 95 lineto
 
524
closepath
 
525
fill
 
526
0.000 0.000 0.000 edgecolor
 
527
newpath 1064 101 moveto
 
528
1075 101 lineto
 
529
1066 95 lineto
 
530
closepath
 
531
stroke
 
532
end grestore
 
533
 
 
534
%       Tacred
 
535
gsave 10 dict begin
 
536
728 18 32 18 ellipse_path
 
537
stroke
 
538
gsave 10 dict begin
 
539
709 13 moveto
 
540
(Tacred)
 
541
[7.44 6.24 6.24 4.56 6.24 6.96]
 
542
xshow
 
543
end grestore
 
544
end grestore
 
545
 
 
546
%       Tacred -> Retyping
 
547
newpath 748 32 moveto
 
548
754 36 759 41 764 45 curveto
 
549
783 63 782 73 800 91 curveto
 
550
802 93 805 95 808 97 curveto
 
551
stroke
 
552
gsave 10 dict begin
 
553
solid
 
554
1 setlinewidth
 
555
0.000 0.000 0.000 edgecolor
 
556
newpath 806 100 moveto
 
557
816 103 lineto
 
558
810 94 lineto
 
559
closepath
 
560
fill
 
561
0.000 0.000 0.000 edgecolor
 
562
newpath 806 100 moveto
 
563
816 103 lineto
 
564
810 94 lineto
 
565
closepath
 
566
stroke
 
567
end grestore
 
568
 
 
569
%       Tacred -> Typing
 
570
newpath 754 29 moveto
 
571
769 35 787 43 803 49 curveto
 
572
stroke
 
573
gsave 10 dict begin
 
574
solid
 
575
1 setlinewidth
 
576
0.000 0.000 0.000 edgecolor
 
577
newpath 802 53 moveto
 
578
813 53 lineto
 
579
805 46 lineto
 
580
closepath
 
581
fill
 
582
0.000 0.000 0.000 edgecolor
 
583
newpath 802 53 moveto
 
584
813 53 lineto
 
585
805 46 lineto
 
586
closepath
 
587
stroke
 
588
end grestore
 
589
 
 
590
%       Cbv
 
591
gsave 10 dict begin
 
592
1246 41 27 18 ellipse_path
 
593
stroke
 
594
gsave 10 dict begin
 
595
1234 36 moveto
 
596
(Cbv)
 
597
[9.36 6.48 6.96]
 
598
xshow
 
599
end grestore
 
600
end grestore
 
601
 
 
602
%       Tacred -> Cbv
 
603
newpath 760 19 moveto
 
604
852 23 1111 35 1209 40 curveto
 
605
stroke
 
606
gsave 10 dict begin
 
607
solid
 
608
1 setlinewidth
 
609
0.000 0.000 0.000 edgecolor
 
610
newpath 1209 44 moveto
 
611
1219 40 lineto
 
612
1209 37 lineto
 
613
closepath
 
614
fill
 
615
0.000 0.000 0.000 edgecolor
 
616
newpath 1209 44 moveto
 
617
1219 40 lineto
 
618
1209 37 lineto
 
619
closepath
 
620
stroke
 
621
end grestore
 
622
 
 
623
%       Evd
 
624
gsave 10 dict begin
 
625
1361 110 27 18 ellipse_path
 
626
stroke
 
627
gsave 10 dict begin
 
628
1349 105 moveto
 
629
(Evd)
 
630
[8.4 6.96 6.96]
 
631
xshow
 
632
end grestore
 
633
end grestore
 
634
 
 
635
%       Cbv -> Evd
 
636
newpath 1266 53 moveto
 
637
1284 64 1312 80 1332 93 curveto
 
638
stroke
 
639
gsave 10 dict begin
 
640
solid
 
641
1 setlinewidth
 
642
0.000 0.000 0.000 edgecolor
 
643
newpath 1331 96 moveto
 
644
1341 98 lineto
 
645
1334 90 lineto
 
646
closepath
 
647
fill
 
648
0.000 0.000 0.000 edgecolor
 
649
newpath 1331 96 moveto
 
650
1341 98 lineto
 
651
1334 90 lineto
 
652
closepath
 
653
stroke
 
654
end grestore
 
655
 
 
656
%       Reductionops
 
657
gsave 10 dict begin
 
658
1246 164 51 18 ellipse_path
 
659
stroke
 
660
gsave 10 dict begin
 
661
1207 159 moveto
 
662
(Reductionops)
 
663
[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96 6.96 6.96 5.52]
 
664
xshow
 
665
end grestore
 
666
end grestore
 
667
 
 
668
%       Inductiveops -> Reductionops
 
669
newpath 1158 164 moveto
 
670
1167 164 1175 164 1184 164 curveto
 
671
stroke
 
672
gsave 10 dict begin
 
673
solid
 
674
1 setlinewidth
 
675
0.000 0.000 0.000 edgecolor
 
676
newpath 1184 168 moveto
 
677
1194 164 lineto
 
678
1184 161 lineto
 
679
closepath
 
680
fill
 
681
0.000 0.000 0.000 edgecolor
 
682
newpath 1184 168 moveto
 
683
1194 164 lineto
 
684
1184 161 lineto
 
685
closepath
 
686
stroke
 
687
end grestore
 
688
 
 
689
%       Reductionops -> Evd
 
690
newpath 1277 150 moveto
 
691
1294 142 1313 133 1330 125 curveto
 
692
stroke
 
693
gsave 10 dict begin
 
694
solid
 
695
1 setlinewidth
 
696
0.000 0.000 0.000 edgecolor
 
697
newpath 1331 128 moveto
 
698
1339 121 lineto
 
699
1328 122 lineto
 
700
closepath
 
701
fill
 
702
0.000 0.000 0.000 edgecolor
 
703
newpath 1331 128 moveto
 
704
1339 121 lineto
 
705
1328 122 lineto
 
706
closepath
 
707
stroke
 
708
end grestore
 
709
 
 
710
%       Termops
 
711
gsave 10 dict begin
 
712
1462 110 37 18 ellipse_path
 
713
stroke
 
714
gsave 10 dict begin
 
715
1437 105 moveto
 
716
(Termops)
 
717
[7.2 6.24 4.8 10.8 6.96 6.96 5.52]
 
718
xshow
 
719
end grestore
 
720
end grestore
 
721
 
 
722
%       Evd -> Termops
 
723
newpath 1388 110 moveto
 
724
1396 110 1405 110 1414 110 curveto
 
725
stroke
 
726
gsave 10 dict begin
 
727
solid
 
728
1 setlinewidth
 
729
0.000 0.000 0.000 edgecolor
 
730
newpath 1414 114 moveto
 
731
1424 110 lineto
 
732
1414 107 lineto
 
733
closepath
 
734
fill
 
735
0.000 0.000 0.000 edgecolor
 
736
newpath 1414 114 moveto
 
737
1424 110 lineto
 
738
1414 107 lineto
 
739
closepath
 
740
stroke
 
741
end grestore
 
742
 
 
743
%       Recordops
 
744
gsave 10 dict begin
 
745
485 24 43 18 ellipse_path
 
746
stroke
 
747
gsave 10 dict begin
 
748
455 19 moveto
 
749
(Recordops)
 
750
[9.12 6.24 6.24 6.96 4.32 6.96 6.96 6.96 5.52]
 
751
xshow
 
752
end grestore
 
753
end grestore
 
754
 
 
755
%       Classops
 
756
gsave 10 dict begin
 
757
610 20 38 18 ellipse_path
 
758
stroke
 
759
gsave 10 dict begin
 
760
584 15 moveto
 
761
(Classops)
 
762
[9.36 3.84 6.24 5.52 5.52 6.96 6.96 5.52]
 
763
xshow
 
764
end grestore
 
765
end grestore
 
766
 
 
767
%       Recordops -> Classops
 
768
newpath 528 23 moveto
 
769
538 22 550 22 561 22 curveto
 
770
stroke
 
771
gsave 10 dict begin
 
772
solid
 
773
1 setlinewidth
 
774
0.000 0.000 0.000 edgecolor
 
775
newpath 561 25 moveto
 
776
571 21 lineto
 
777
561 19 lineto
 
778
closepath
 
779
fill
 
780
0.000 0.000 0.000 edgecolor
 
781
newpath 561 25 moveto
 
782
571 21 lineto
 
783
561 19 lineto
 
784
closepath
 
785
stroke
 
786
end grestore
 
787
 
 
788
%       Classops -> Tacred
 
789
newpath 649 19 moveto
 
790
661 19 674 19 686 19 curveto
 
791
stroke
 
792
gsave 10 dict begin
 
793
solid
 
794
1 setlinewidth
 
795
0.000 0.000 0.000 edgecolor
 
796
newpath 686 23 moveto
 
797
696 19 lineto
 
798
686 16 lineto
 
799
closepath
 
800
fill
 
801
0.000 0.000 0.000 edgecolor
 
802
newpath 686 23 moveto
 
803
696 19 lineto
 
804
686 16 lineto
 
805
closepath
 
806
stroke
 
807
end grestore
 
808
 
 
809
%       Rawterm -> Evd
 
810
newpath 1148 110 moveto
 
811
1196 110 1277 110 1324 110 curveto
 
812
stroke
 
813
gsave 10 dict begin
 
814
solid
 
815
1 setlinewidth
 
816
0.000 0.000 0.000 edgecolor
 
817
newpath 1324 114 moveto
 
818
1334 110 lineto
 
819
1324 107 lineto
 
820
closepath
 
821
fill
 
822
0.000 0.000 0.000 edgecolor
 
823
newpath 1324 114 moveto
 
824
1334 110 lineto
 
825
1324 107 lineto
 
826
closepath
 
827
stroke
 
828
end grestore
 
829
 
 
830
%       Pretyping
 
831
gsave 10 dict begin
 
832
40 183 40 18 ellipse_path
 
833
stroke
 
834
gsave 10 dict begin
 
835
13 178 moveto
 
836
(Pretyping)
 
837
[7.68 4.56 6 3.84 6.96 6.96 3.84 6.96 6.96]
 
838
xshow
 
839
end grestore
 
840
end grestore
 
841
 
 
842
%       Pretyping -> Pattern
 
843
newpath 78 189 moveto
 
844
121 194 191 202 251 202 curveto
 
845
251 202 251 202 485 202 curveto
 
846
556 202 636 205 685 208 curveto
 
847
stroke
 
848
gsave 10 dict begin
 
849
solid
 
850
1 setlinewidth
 
851
0.000 0.000 0.000 edgecolor
 
852
newpath 685 212 moveto
 
853
695 208 lineto
 
854
685 205 lineto
 
855
closepath
 
856
fill
 
857
0.000 0.000 0.000 edgecolor
 
858
newpath 685 212 moveto
 
859
695 208 lineto
 
860
685 205 lineto
 
861
closepath
 
862
stroke
 
863
end grestore
 
864
 
 
865
%       Cases
 
866
gsave 10 dict begin
 
867
146 64 30 18 ellipse_path
 
868
stroke
 
869
gsave 10 dict begin
 
870
129 59 moveto
 
871
(Cases)
 
872
[9.36 6.24 5.52 6.24 5.52]
 
873
xshow
 
874
end grestore
 
875
end grestore
 
876
 
 
877
%       Pretyping -> Cases
 
878
newpath 53 166 moveto
 
879
68 147 93 115 116 91 curveto
 
880
118 89 119 88 121 86 curveto
 
881
stroke
 
882
gsave 10 dict begin
 
883
solid
 
884
1 setlinewidth
 
885
0.000 0.000 0.000 edgecolor
 
886
newpath 124 88 moveto
 
887
129 79 lineto
 
888
119 83 lineto
 
889
closepath
 
890
fill
 
891
0.000 0.000 0.000 edgecolor
 
892
newpath 124 88 moveto
 
893
129 79 lineto
 
894
119 83 lineto
 
895
closepath
 
896
stroke
 
897
end grestore
 
898
 
 
899
%       Detyping
 
900
gsave 10 dict begin
 
901
969 164 39 18 ellipse_path
 
902
stroke
 
903
gsave 10 dict begin
 
904
942 159 moveto
 
905
(Detyping)
 
906
[10.08 6 3.84 6.96 6.96 3.84 6.96 6.96]
 
907
xshow
 
908
end grestore
 
909
end grestore
 
910
 
 
911
%       Pretyping -> Detyping
 
912
newpath 78 177 moveto
 
913
121 172 191 164 251 164 curveto
 
914
251 164 251 164 728 164 curveto
 
915
794 164 870 164 919 164 curveto
 
916
stroke
 
917
gsave 10 dict begin
 
918
solid
 
919
1 setlinewidth
 
920
0.000 0.000 0.000 edgecolor
 
921
newpath 919 168 moveto
 
922
929 164 lineto
 
923
919 161 lineto
 
924
closepath
 
925
fill
 
926
0.000 0.000 0.000 edgecolor
 
927
newpath 919 168 moveto
 
928
929 164 lineto
 
929
919 161 lineto
 
930
closepath
 
931
stroke
 
932
end grestore
 
933
 
 
934
%       Indrec
 
935
gsave 10 dict begin
 
936
251 271 31 18 ellipse_path
 
937
stroke
 
938
gsave 10 dict begin
 
939
233 266 moveto
 
940
(Indrec)
 
941
[4.56 6.96 6.96 4.56 6.24 6.24]
 
942
xshow
 
943
end grestore
 
944
end grestore
 
945
 
 
946
%       Pretyping -> Indrec
 
947
newpath 69 195 moveto
 
948
83 202 101 209 116 216 curveto
 
949
150 230 188 246 216 257 curveto
 
950
stroke
 
951
gsave 10 dict begin
 
952
solid
 
953
1 setlinewidth
 
954
0.000 0.000 0.000 edgecolor
 
955
newpath 214 260 moveto
 
956
225 261 lineto
 
957
217 254 lineto
 
958
closepath
 
959
fill
 
960
0.000 0.000 0.000 edgecolor
 
961
newpath 214 260 moveto
 
962
225 261 lineto
 
963
217 254 lineto
 
964
closepath
 
965
stroke
 
966
end grestore
 
967
 
 
968
%       Coercion
 
969
gsave 10 dict begin
 
970
251 67 39 18 ellipse_path
 
971
stroke
 
972
gsave 10 dict begin
 
973
225 62 moveto
 
974
(Coercion)
 
975
[9.36 6.96 6.24 4.56 6.24 3.84 6.96 6.96]
 
976
xshow
 
977
end grestore
 
978
end grestore
 
979
 
 
980
%       Cases -> Coercion
 
981
newpath 176 65 moveto
 
982
184 65 193 66 202 66 curveto
 
983
stroke
 
984
gsave 10 dict begin
 
985
solid
 
986
1 setlinewidth
 
987
0.000 0.000 0.000 edgecolor
 
988
newpath 202 70 moveto
 
989
212 66 lineto
 
990
202 63 lineto
 
991
closepath
 
992
fill
 
993
0.000 0.000 0.000 edgecolor
 
994
newpath 202 70 moveto
 
995
212 66 lineto
 
996
202 63 lineto
 
997
closepath
 
998
stroke
 
999
end grestore
 
1000
 
 
1001
%       Detyping -> Inductiveops
 
1002
newpath 1009 164 moveto
 
1003
1022 164 1036 164 1050 164 curveto
 
1004
stroke
 
1005
gsave 10 dict begin
 
1006
solid
 
1007
1 setlinewidth
 
1008
0.000 0.000 0.000 edgecolor
 
1009
newpath 1050 168 moveto
 
1010
1060 164 lineto
 
1011
1050 161 lineto
 
1012
closepath
 
1013
fill
 
1014
0.000 0.000 0.000 edgecolor
 
1015
newpath 1050 168 moveto
 
1016
1060 164 lineto
 
1017
1050 161 lineto
 
1018
closepath
 
1019
stroke
 
1020
end grestore
 
1021
 
 
1022
%       Detyping -> Rawterm
 
1023
newpath 999 152 moveto
 
1024
1020 144 1047 133 1069 125 curveto
 
1025
stroke
 
1026
gsave 10 dict begin
 
1027
solid
 
1028
1 setlinewidth
 
1029
0.000 0.000 0.000 edgecolor
 
1030
newpath 1070 128 moveto
 
1031
1079 122 lineto
 
1032
1068 122 lineto
 
1033
closepath
 
1034
fill
 
1035
0.000 0.000 0.000 edgecolor
 
1036
newpath 1070 128 moveto
 
1037
1079 122 lineto
 
1038
1068 122 lineto
 
1039
closepath
 
1040
stroke
 
1041
end grestore
 
1042
 
 
1043
%       Indrec -> Inductiveops
 
1044
newpath 281 276 moveto
 
1045
325 283 412 294 485 294 curveto
 
1046
485 294 485 294 839 294 curveto
 
1047
937 294 1036 225 1082 188 curveto
 
1048
stroke
 
1049
gsave 10 dict begin
 
1050
solid
 
1051
1 setlinewidth
 
1052
0.000 0.000 0.000 edgecolor
 
1053
newpath 1085 190 moveto
 
1054
1090 181 lineto
 
1055
1080 185 lineto
 
1056
closepath
 
1057
fill
 
1058
0.000 0.000 0.000 edgecolor
 
1059
newpath 1085 190 moveto
 
1060
1090 181 lineto
 
1061
1080 185 lineto
 
1062
closepath
 
1063
stroke
 
1064
end grestore
 
1065
 
 
1066
%       Matching
 
1067
gsave 10 dict begin
 
1068
610 248 40 18 ellipse_path
 
1069
stroke
 
1070
gsave 10 dict begin
 
1071
582 243 moveto
 
1072
(Matching)
 
1073
[12.48 6.24 3.84 6 6.96 3.84 6.96 6.96]
 
1074
xshow
 
1075
end grestore
 
1076
end grestore
 
1077
 
 
1078
%       Matching -> Pattern
 
1079
newpath 643 237 moveto
 
1080
658 232 675 227 689 222 curveto
 
1081
stroke
 
1082
gsave 10 dict begin
 
1083
solid
 
1084
1 setlinewidth
 
1085
0.000 0.000 0.000 edgecolor
 
1086
newpath 690 225 moveto
 
1087
699 219 lineto
 
1088
688 219 lineto
 
1089
closepath
 
1090
fill
 
1091
0.000 0.000 0.000 edgecolor
 
1092
newpath 690 225 moveto
 
1093
699 219 lineto
 
1094
688 219 lineto
 
1095
closepath
 
1096
stroke
 
1097
end grestore
 
1098
 
 
1099
%       Matching -> Reductionops
 
1100
newpath 650 250 moveto
 
1101
696 253 773 256 839 256 curveto
 
1102
839 256 839 256 969 256 curveto
 
1103
1059 256 1159 212 1210 184 curveto
 
1104
stroke
 
1105
gsave 10 dict begin
 
1106
solid
 
1107
1 setlinewidth
 
1108
0.000 0.000 0.000 edgecolor
 
1109
newpath 1212 187 moveto
 
1110
1219 179 lineto
 
1111
1209 181 lineto
 
1112
closepath
 
1113
fill
 
1114
0.000 0.000 0.000 edgecolor
 
1115
newpath 1212 187 moveto
 
1116
1219 179 lineto
 
1117
1209 181 lineto
 
1118
closepath
 
1119
stroke
 
1120
end grestore
 
1121
 
 
1122
%       Evarconv
 
1123
gsave 10 dict begin
 
1124
366 67 40 18 ellipse_path
 
1125
stroke
 
1126
gsave 10 dict begin
 
1127
339 62 moveto
 
1128
(Evarconv)
 
1129
[8.4 6.72 6.24 4.56 6.24 6.96 6.48 6.96]
 
1130
xshow
 
1131
end grestore
 
1132
end grestore
 
1133
 
 
1134
%       Evarconv -> Evarutil
 
1135
newpath 406 68 moveto
 
1136
474 69 610 71 682 72 curveto
 
1137
stroke
 
1138
gsave 10 dict begin
 
1139
solid
 
1140
1 setlinewidth
 
1141
0.000 0.000 0.000 edgecolor
 
1142
newpath 682 76 moveto
 
1143
692 72 lineto
 
1144
682 69 lineto
 
1145
closepath
 
1146
fill
 
1147
0.000 0.000 0.000 edgecolor
 
1148
newpath 682 76 moveto
 
1149
692 72 lineto
 
1150
682 69 lineto
 
1151
closepath
 
1152
stroke
 
1153
end grestore
 
1154
 
 
1155
%       Evarconv -> Recordops
 
1156
newpath 397 56 moveto
 
1157
411 51 428 45 442 39 curveto
 
1158
stroke
 
1159
gsave 10 dict begin
 
1160
solid
 
1161
1 setlinewidth
 
1162
0.000 0.000 0.000 edgecolor
 
1163
newpath 443 42 moveto
 
1164
452 36 lineto
 
1165
441 36 lineto
 
1166
closepath
 
1167
fill
 
1168
0.000 0.000 0.000 edgecolor
 
1169
newpath 443 42 moveto
 
1170
452 36 lineto
 
1171
441 36 lineto
 
1172
closepath
 
1173
stroke
 
1174
end grestore
 
1175
 
 
1176
%       Coercion -> Evarconv
 
1177
newpath 290 67 moveto
 
1178
299 67 307 67 316 67 curveto
 
1179
stroke
 
1180
gsave 10 dict begin
 
1181
solid
 
1182
1 setlinewidth
 
1183
0.000 0.000 0.000 edgecolor
 
1184
newpath 316 71 moveto
 
1185
326 67 lineto
 
1186
316 64 lineto
 
1187
closepath
 
1188
fill
 
1189
0.000 0.000 0.000 edgecolor
 
1190
newpath 316 71 moveto
 
1191
326 67 lineto
 
1192
316 64 lineto
 
1193
closepath
 
1194
stroke
 
1195
end grestore
 
1196
 
 
1197
%       Clenv
 
1198
gsave 10 dict begin
 
1199
146 118 30 18 ellipse_path
 
1200
stroke
 
1201
gsave 10 dict begin
 
1202
129 113 moveto
 
1203
(Clenv)
 
1204
[9.36 3.84 6.24 6.48 6.96]
 
1205
xshow
 
1206
end grestore
 
1207
end grestore
 
1208
 
 
1209
%       Clenv -> Unification
 
1210
newpath 176 118 moveto
 
1211
252 118 455 118 554 118 curveto
 
1212
stroke
 
1213
gsave 10 dict begin
 
1214
solid
 
1215
1 setlinewidth
 
1216
0.000 0.000 0.000 edgecolor
 
1217
newpath 554 122 moveto
 
1218
564 118 lineto
 
1219
554 115 lineto
 
1220
closepath
 
1221
fill
 
1222
0.000 0.000 0.000 edgecolor
 
1223
newpath 554 122 moveto
 
1224
564 118 lineto
 
1225
554 115 lineto
 
1226
closepath
 
1227
stroke
 
1228
end grestore
 
1229
 
 
1230
%       Clenv -> Coercion
 
1231
newpath 170 107 moveto
 
1232
183 100 200 93 215 85 curveto
 
1233
stroke
 
1234
gsave 10 dict begin
 
1235
solid
 
1236
1 setlinewidth
 
1237
0.000 0.000 0.000 edgecolor
 
1238
newpath 217 88 moveto
 
1239
224 80 lineto
 
1240
214 82 lineto
 
1241
closepath
 
1242
fill
 
1243
0.000 0.000 0.000 edgecolor
 
1244
newpath 217 88 moveto
 
1245
224 80 lineto
 
1246
214 82 lineto
 
1247
closepath
 
1248
stroke
 
1249
end grestore
 
1250
endpage
 
1251
showpage
 
1252
grestore
 
1253
%%PageTrailer
 
1254
%%EndPage: 1
 
1255
%%Trailer
 
1256
%%Pages: 1
 
1257
end
 
1258
restore
 
1259
%%EOF