Remove generatable documentation files from repository. (Fix bug #4315)

6 files changed, 0 insertions, 511 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index c8dd220baf..fbb866e875 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -509,22 +509,14 @@ library. (Statements in boldface are the most ``interesting'' ones for
 Coq.) The justification of their validity relies on the interpretability
 in set theory.
 
-% fig2dev -m 2 -L png axioms.fig axioms.png
-% fig2dev -L pdftex axioms.fig axioms.pdf
-% fig2dev -L pdftex_t -p axioms.pdf axioms.fig axioms.pdf_t
-% fig2dev -L pstex axioms.fig axioms.eps
-% fig2dev -L pstex_t -p axioms.eps axioms.fig axioms.eps_t
-
 \begin{figure}[htbp]
 %HEVEA\imgsrc{axioms.png}
 %BEGIN LATEX
 \begin{center}
 \ifpdf   % si on est en pdflatex
 \scalebox{0.65}{\input{axioms.pdf_t}}
-%\includegraphics[width=1.0\textwidth]{axioms.png}
 \else
 \scalebox{0.65}{\input{axioms.eps_t}}
-%\includegraphics[width=1.0\textwidth]{axioms.eps}
 \fi
 \end{center}
 %END LATEX
diff --git a/doc/faq/axioms.eps b/doc/faq/axioms.eps
deleted file mode 100644
index 836afc3474..0000000000
--- a/doc/faq/axioms.eps
+++ /dev/null
@@ -1,417 +0,0 @@
-%!PS-Adobe-3.0 EPSF-3.0
-%%Title: axioms.fig
-%%Creator: fig2dev Version 3.2 Patchlevel 5e
-%%CreationDate: Sun Jul 26 08:23:54 2015
-%%BoundingBox: 0 0 647 514
-%Magnification: 1.0000
-%%EndComments
-%%BeginProlog
-/$F2psDict 200 dict def
-$F2psDict begin
-$F2psDict /mtrx matrix put
-/col-1 {0 setgray} bind def
-/col0 {0.000 0.000 0.000 srgb} bind def
-/col1 {0.000 0.000 1.000 srgb} bind def
-/col2 {0.000 1.000 0.000 srgb} bind def
-/col3 {0.000 1.000 1.000 srgb} bind def
-/col4 {1.000 0.000 0.000 srgb} bind def
-/col5 {1.000 0.000 1.000 srgb} bind def
-/col6 {1.000 1.000 0.000 srgb} bind def
-/col7 {1.000 1.000 1.000 srgb} bind def
-/col8 {0.000 0.000 0.560 srgb} bind def
-/col9 {0.000 0.000 0.690 srgb} bind def
-/col10 {0.000 0.000 0.820 srgb} bind def
-/col11 {0.530 0.810 1.000 srgb} bind def
-/col12 {0.000 0.560 0.000 srgb} bind def
-/col13 {0.000 0.690 0.000 srgb} bind def
-/col14 {0.000 0.820 0.000 srgb} bind def
-/col15 {0.000 0.560 0.560 srgb} bind def
-/col16 {0.000 0.690 0.690 srgb} bind def
-/col17 {0.000 0.820 0.820 srgb} bind def
-/col18 {0.560 0.000 0.000 srgb} bind def
-/col19 {0.690 0.000 0.000 srgb} bind def
-/col20 {0.820 0.000 0.000 srgb} bind def
-/col21 {0.560 0.000 0.560 srgb} bind def
-/col22 {0.690 0.000 0.690 srgb} bind def
-/col23 {0.820 0.000 0.820 srgb} bind def
-/col24 {0.500 0.190 0.000 srgb} bind def
-/col25 {0.630 0.250 0.000 srgb} bind def
-/col26 {0.750 0.380 0.000 srgb} bind def
-/col27 {1.000 0.500 0.500 srgb} bind def
-/col28 {1.000 0.630 0.630 srgb} bind def
-/col29 {1.000 0.750 0.750 srgb} bind def
-/col30 {1.000 0.880 0.880 srgb} bind def
-/col31 {1.000 0.840 0.000 srgb} bind def
-
-end
-
-/cp {closepath} bind def
-/ef {eofill} bind def
-/gr {grestore} bind def
-/gs {gsave} bind def
-/sa {save} bind def
-/rs {restore} bind def
-/l {lineto} bind def
-/m {moveto} bind def
-/rm {rmoveto} bind def
-/n {newpath} bind def
-/s {stroke} bind def
-/sh {show} bind def
-/slc {setlinecap} bind def
-/slj {setlinejoin} bind def
-/slw {setlinewidth} bind def
-/srgb {setrgbcolor} bind def
-/rot {rotate} bind def
-/sc {scale} bind def
-/sd {setdash} bind def
-/ff {findfont} bind def
-/sf {setfont} bind def
-/scf {scalefont} bind def
-/sw {stringwidth} bind def
-/tr {translate} bind def
-/tnt {dup dup currentrgbcolor
-  4 -2 roll dup 1 exch sub 3 -1 roll mul add
-  4 -2 roll dup 1 exch sub 3 -1 roll mul add
-  4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb}
-  bind def
-/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul
-  4 -2 roll mul srgb} bind def
-/$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def
-/$F2psEnd {$F2psEnteredState restore end} def
-
-/pageheader {
-save
-newpath 0 514 moveto 0 0 lineto 647 0 lineto 647 514 lineto closepath clip newpath
--26.1 566.6 translate
-1 -1 scale
-$F2psBegin
-10 setmiterlimit
-0 slj 0 slc
- 0.06000 0.06000 sc
-} bind def
-/pagefooter {
-$F2psEnd
-restore
-} bind def
-%%EndProlog
-pageheader
-%
-% Fig objects follow
-%
-% 
-% here starts figure with depth 50
-% Arc
-7.500 slw
-0 slc
-gs  clippath
-4188 5861 m 4168 6010 l 4227 6018 l 4247 5869 l 4247 5869 l 4202 5984 l 4188 5861 l cp
-eoclip
-n 14032.5 7222.5 9908.2 -159.9465 -172.9126 arcn
-gs col0 s gr
- gr
-
-% arrowhead
-0 slj
-n 4188 5861 m 4202 5984 l 4247 5869 l 4188 5861 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3465 9040 m 3599 9108 l 3626 9054 l 3492 8987 l 3492 8987 l 3586 9068 l 3465 9040 l cp
-eoclip
-n 3600.0 8925.0 150.0 90.0000 -90.0000 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3465 8740 m 3599 8808 l 3626 8754 l 3492 8687 l 3492 8687 l 3586 8768 l 3465 8740 l cp
-eoclip
-n 3600.0 8625.0 150.0 90.0000 -90.0000 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3492 8262 m 3626 8195 l 3599 8141 l 3465 8209 l 3465 8209 l 3586 8182 l 3492 8262 l cp
-3465 8440 m 3599 8508 l 3626 8454 l 3492 8387 l 3492 8387 l 3586 8468 l 3465 8440 l cp
-eoclip
-n 3600.0 8325.0 150.0 90.0000 -90.0000 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3465 8440 m 3586 8468 l 3492 8387 l 3465 8440 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3492 8262 m 3586 8182 l 3465 8209 l 3492 8262 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3492 8562 m 3626 8495 l 3599 8441 l 3465 8509 l 3465 8509 l 3586 8482 l 3492 8562 l cp
-3465 8740 m 3599 8808 l 3626 8754 l 3492 8687 l 3492 8687 l 3586 8768 l 3465 8740 l cp
-eoclip
-n 3600.0 8625.0 150.0 90.0000 -90.0000 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3492 8562 m 3586 8482 l 3465 8509 l 3492 8562 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3492 8862 m 3626 8795 l 3599 8741 l 3465 8809 l 3465 8809 l 3586 8782 l 3492 8862 l cp
-3465 9040 m 3599 9108 l 3626 9054 l 3492 8987 l 3492 8987 l 3586 9068 l 3465 9040 l cp
-eoclip
-n 3600.0 8925.0 150.0 90.0000 -90.0000 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3492 8862 m 3586 8782 l 3465 8809 l 3492 8862 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3492 9162 m 3626 9095 l 3599 9041 l 3465 9109 l 3465 9109 l 3586 9082 l 3492 9162 l cp
-3465 9340 m 3599 9408 l 3626 9354 l 3492 9287 l 3492 9287 l 3586 9368 l 3465 9340 l cp
-eoclip
-n 3600.0 9225.0 150.0 90.0000 -90.0000 arc
-gs col0 s gr
- gr
-
-% arrowhead
-n 3465 9340 m 3586 9368 l 3492 9287 l 3465 9340 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3492 9162 m 3586 9082 l 3465 9109 l 3492 9162 l  cp gs 0.00 setgray ef gr  col0 s
-% Arc
-gs  clippath
-3733 7095 m 3805 7227 l 3858 7198 l 3785 7066 l 3785 7066 l 3817 7186 l 3733 7095 l cp
-eoclip
-n 6309.5 5767.7 2867.8 -137.3570 150.0374 arcn
-gs col0 s gr
- gr
-
-% arrowhead
-n 3733 7095 m 3817 7186 l 3785 7066 l 3733 7095 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-7204 5860 m 7167 6007 l 7225 6021 l 7262 5874 l 7262 5874 l 7204 5984 l 7204 5860 l cp
-eoclip
-n 7725 3900 m
- 7200 6000 l gs col0 s gr gr
-
-% arrowhead
-n 7204 5860 m 7204 5984 l 7262 5874 l 7204 5860 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-7170 6914 m 7170 7065 l 7230 7065 l 7230 6914 l 7230 6914 l 7200 7034 l 7170 6914 l cp
-eoclip
-n 7200 6225 m
- 7200 7050 l gs col0 s gr gr
-
-% arrowhead
-n 7170 6914 m 7200 7034 l 7230 6914 l 7170 6914 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-5520 5864 m 5520 6015 l 5580 6015 l 5580 5864 l 5580 5864 l 5550 5984 l 5520 5864 l cp
-5580 5761 m 5580 5610 l 5520 5610 l 5520 5761 l 5520 5761 l 5550 5641 l 5580 5761 l cp
-eoclip
-n 5550 5625 m
- 5550 6000 l gs col0 s gr gr
-
-% arrowhead
-n 5580 5761 m 5550 5641 l 5520 5761 l 5580 5761 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 5520 5864 m 5550 5984 l 5580 5864 l 5520 5864 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-3345 3464 m 3345 3615 l 3405 3615 l 3405 3464 l 3405 3464 l 3375 3584 l 3345 3464 l cp
-3405 3361 m 3405 3210 l 3345 3210 l 3345 3361 l 3345 3361 l 3375 3241 l 3405 3361 l cp
-eoclip
-n 3375 3225 m
- 3375 3600 l gs col0 s gr gr
-
-% arrowhead
-n 3405 3361 m 3375 3241 l 3345 3361 l 3405 3361 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3345 3464 m 3375 3584 l 3405 3464 l 3345 3464 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-3344 2114 m 3346 2265 l 3406 2264 l 3404 2113 l 3404 2113 l 3376 2234 l 3344 2114 l cp
-eoclip
-n 3373 1950 m
- 3376 2250 l gs col0 s gr gr
-
-% arrowhead
-n 3344 2114 m 3376 2234 l 3404 2113 l 3344 2114 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-3345 2864 m 3345 3015 l 3405 3015 l 3405 2864 l 3405 2864 l 3375 2984 l 3345 2864 l cp
-3405 2761 m 3405 2610 l 3345 2610 l 3345 2761 l 3345 2761 l 3375 2641 l 3405 2761 l cp
-eoclip
-n 3375 2625 m
- 3375 3000 l gs col0 s gr gr
-
-% arrowhead
-n 3405 2761 m 3375 2641 l 3345 2761 l 3405 2761 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 3345 2864 m 3375 2984 l 3405 2864 l 3345 2864 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-n 2175 3600 m
- 3750 3600 l gs col0 s gr 
-% Polyline
-gs  clippath
-2611 2445 m 2460 2445 l 2460 2505 l 2611 2505 l 2611 2505 l 2491 2475 l 2611 2445 l cp
-eoclip
-n 3075 2475 m
- 2475 2475 l gs col0 s gr gr
-
-% arrowhead
-n 2611 2445 m 2491 2475 l 2611 2505 l 2611 2445 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-3345 1289 m 3347 1440 l 3407 1439 l 3405 1288 l 3405 1288 l 3377 1409 l 3345 1289 l cp
-eoclip
-n 3374 1125 m
- 3377 1425 l gs col0 s gr gr
-
-% arrowhead
-n 3345 1289 m 3377 1409 l 3405 1288 l 3345 1289 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-1711 945 m 1560 945 l 1560 1005 l 1711 1005 l 1711 1005 l 1591 975 l 1711 945 l cp
-eoclip
-n 3075 975 m
- 1575 975 l gs col0 s gr gr
-
-% arrowhead
-n 1711 945 m 1591 975 l 1711 1005 l 1711 945 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-2161 1695 m 2010 1695 l 2010 1755 l 2161 1755 l 2161 1755 l 2041 1725 l 2161 1695 l cp
-eoclip
-n 3075 1725 m
- 2025 1725 l gs col0 s gr gr
-
-% arrowhead
-n 2161 1695 m 2041 1725 l 2161 1755 l 2161 1695 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-n 8025 5925 m 8250 5925 l 9000 4950 l
- 9150 4950 l gs col0 s gr 
-% Polyline
-gs  clippath
-8312 4025 m 8275 3878 l 8217 3892 l 8254 4039 l 8254 4039 l 8254 3916 l 8312 4025 l cp
-eoclip
-n 8625 5400 m
- 8250 3900 l gs col0 s gr gr
-
-% arrowhead
-n 8312 4025 m 8254 3916 l 8254 4039 l 8312 4025 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-4700 7888 m 4553 7924 l 4567 7982 l 4714 7946 l 4714 7946 l 4591 7946 l 4700 7888 l cp
-eoclip
-n 7050 7350 m
- 4575 7950 l gs col0 s gr gr
-
-% arrowhead
-n 4700 7888 m 4591 7946 l 4714 7946 l 4700 7888 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-4170 7814 m 4170 7965 l 4230 7965 l 4230 7814 l 4230 7814 l 4200 7934 l 4170 7814 l cp
-eoclip
-n 4200 7500 m
- 4200 7950 l gs col0 s gr gr
-
-% arrowhead
-n 4170 7814 m 4200 7934 l 4230 7814 l 4170 7814 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-1295 3398 m 1339 3543 l 1397 3526 l 1353 3381 l 1353 3381 l 1359 3505 l 1295 3398 l cp
-1207 2893 m 1163 2748 l 1105 2765 l 1149 2910 l 1149 2910 l 1144 2787 l 1207 2893 l cp
-eoclip
-n 1139 2771 m
- 1364 3521 l gs col0 s gr gr
-
-% arrowhead
-n 1207 2893 m 1144 2787 l 1149 2910 l 1207 2893 l  cp gs 0.00 setgray ef gr  col0 s
-% arrowhead
-n 1295 3398 m 1359 3505 l 1353 3381 l 1295 3398 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-n 4425 4875 m
- 7350 3825 l gs col0 s gr 
-% Polyline
-gs  clippath
-1019 1289 m 1021 1440 l 1081 1439 l 1079 1288 l 1079 1288 l 1051 1409 l 1019 1289 l cp
-eoclip
-n 1048 1125 m
- 1051 1425 l gs col0 s gr gr
-
-% arrowhead
-n 1019 1289 m 1051 1409 l 1079 1288 l 1019 1289 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-1020 2114 m 1022 2265 l 1082 2264 l 1080 2113 l 1080 2113 l 1052 2234 l 1020 2114 l cp
-eoclip
-n 1049 1950 m
- 1052 2250 l gs col0 s gr gr
-
-% arrowhead
-n 1020 2114 m 1052 2234 l 1080 2113 l 1020 2114 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-2104 5879 m 2151 6023 l 2208 6005 l 2161 5861 l 2161 5861 l 2170 5985 l 2104 5879 l cp
-eoclip
-n 1500 3900 m
- 2175 6000 l gs col0 s gr gr
-
-% arrowhead
-n 2104 5879 m 2170 5985 l 2161 5861 l 2104 5879 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-n 4575 6000 m
- 6450 6000 l gs col0 s gr 
-% Polyline
-gs  clippath
-6900 7063 m 7043 7113 l 7063 7056 l 6920 7006 l 6920 7006 l 7024 7075 l 6900 7063 l cp
-eoclip
-n 4714 6255 m
- 7039 7080 l gs col0 s gr gr
-
-% arrowhead
-n 6900 7063 m 7024 7075 l 6920 7006 l 6900 7063 l  cp gs 0.00 setgray ef gr  col0 s
-% Polyline
-gs  clippath
-4170 7064 m 4170 7215 l 4230 7215 l 4230 7064 l 4230 7064 l 4200 7184 l 4170 7064 l cp
-eoclip
-n 4200 6225 m
- 4200 7200 l gs col-1 s gr gr
-
-% arrowhead
-n 4170 7064 m 4200 7184 l 4230 7064 l 4170 7064 l  cp gs 0.00 setgray ef gr  col-1 s
-% Polyline
-2 slj
-n 6450 7050 m 6448 7050 l 6444 7049 l 6437 7048 l 6425 7046 l 6408 7044 l
- 6385 7040 l 6356 7036 l 6320 7030 l 6279 7024 l 6231 7017 l
- 6177 7008 l 6118 6999 l 6054 6990 l 5986 6979 l 5915 6969 l
- 5841 6958 l 5766 6946 l 5690 6935 l 5614 6924 l 5539 6913 l
- 5464 6902 l 5391 6891 l 5320 6881 l 5252 6871 l 5185 6861 l
- 5122 6852 l 5061 6843 l 5002 6835 l 4947 6827 l 4894 6820 l
- 4843 6813 l 4796 6807 l 4750 6801 l 4707 6796 l 4666 6791 l
- 4627 6786 l 4590 6782 l 4555 6778 l 4521 6774 l 4489 6771 l
- 4458 6768 l 4429 6765 l 4400 6763 l 4350 6759 l 4303 6755 l
- 4258 6753 l 4216 6751 l 4176 6751 l 4138 6750 l 4102 6751 l
- 4068 6752 l 4037 6754 l 4008 6757 l 3980 6760 l 3955 6764 l
- 3933 6768 l 3912 6773 l 3894 6778 l 3877 6784 l 3863 6790 l
- 3850 6796 l 3839 6803 l 3829 6810 l 3820 6816 l 3813 6823 l
- 3806 6830 l 3800 6838 l 3791 6850 l 3783 6863 l 3776 6878 l
- 3771 6894 l 3766 6912 l 3762 6932 l 3759 6954 l 3756 6977 l
- 3753 7000 l 3752 7021 l 3751 7036 l 3750 7045 l 3750 7049 l
-
- 3750 7050 l gs col0 s gr 
-% here ends figure;
-pagefooter
-showpage
-%%Trailer
-%EOF
diff --git a/doc/faq/axioms.eps_t b/doc/faq/axioms.eps_t
deleted file mode 100644
index 38f1a3fed4..0000000000
--- a/doc/faq/axioms.eps_t
+++ /dev/null
@@ -1,43 +0,0 @@
-\begin{picture}(0,0)%
-\includegraphics{axioms.eps}%
-\end{picture}%
-\setlength{\unitlength}{3947sp}%
-%
-\begingroup\makeatletter\ifx\SetFigFont\undefined%
-\gdef\SetFigFont#1#2#3#4#5{%
-  \reset@font\fontsize{#1}{#2pt}%
-  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
-  \selectfont}%
-\fi\endgroup%
-\begin{picture}(10779,8553)(436,-8605)
-\put(3676,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Excluded-middle}}}}
-\put(451,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Operator iota}}}}
-\put(3151,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive indefinite description}}}}
-\put(3151,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}}
-\put(451,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive definite descr.}}}}
-\put(451,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}}
-\put(3826,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Relational choice axiom}}}}
-\put(6901,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Predicate extensionality}}}}
-\put(1276,-4186){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(if Set impredicative)}}}}
-\put(3751,-4411){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Diaconescu)}}}}
-\put(4951,-4711){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional degeneracy}}}}
-\put(6151,-5311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional extensionality}}}}
-\put(4951,-5686){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(needs Prop-impredicativity)}}}}
-\put(6001,-5911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Berardi)}}}}
-\put(1576,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Not excluded-middle}}}}
-\put(3376,-6586){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Decidability of equality on any A}}}}
-\put(3601,-7336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Axiom K on A}}}}
-\put(3601,-7636){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of reflexivity proofs for equality on A}}}}
-\put(3601,-7936){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of equality proofs on A}}}}
-\put(3601,-8536){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Invariance by substitution of reflexivity proofs for equality on A}}}}
-\put(9001,-4336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional extensionality}}}}
-\put(3601,-8236){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Injectivity of equality on Sigma-types on A}}}}
-\put(6451,-6436){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Proof-irrelevance}}}}
-\put(3151,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Operator epsilon}}}}
-\put(3151,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}}
-\put(3151,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}indefinite description}}}}
-\put(3151,-2311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional choice axiom}}}}
-\put(451,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}}
-\put(451,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}definite description}}}}
-\put(451,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Axiom of unique choice}}}}
-\end{picture}%
diff --git a/doc/faq/axioms.pdf b/doc/faq/axioms.pdf
deleted file mode 100644
index 2ba5bf85b6..0000000000
--- a/doc/faq/axioms.pdf
+++ /dev/null
diff --git a/doc/faq/axioms.pdf_t b/doc/faq/axioms.pdf_t
deleted file mode 100644
index 06dc4b280d..0000000000
--- a/doc/faq/axioms.pdf_t
+++ /dev/null
@@ -1,43 +0,0 @@
-\begin{picture}(0,0)%
-\includegraphics{axioms.pdf}%
-\end{picture}%
-\setlength{\unitlength}{3947sp}%
-%
-\begingroup\makeatletter\ifx\SetFigFont\undefined%
-\gdef\SetFigFont#1#2#3#4#5{%
-  \reset@font\fontsize{#1}{#2pt}%
-  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
-  \selectfont}%
-\fi\endgroup%
-\begin{picture}(10779,8553)(436,-8605)
-\put(3676,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Excluded-middle}}}}
-\put(451,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Operator iota}}}}
-\put(3151,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive indefinite description}}}}
-\put(3151,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}}
-\put(451,-1561){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Constructive definite descr.}}}}
-\put(451,-1786){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}in propositional context}}}}
-\put(3826,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Relational choice axiom}}}}
-\put(6901,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Predicate extensionality}}}}
-\put(1276,-4186){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(if Set impredicative)}}}}
-\put(3751,-4411){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Diaconescu)}}}}
-\put(4951,-4711){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional degeneracy}}}}
-\put(6151,-5311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Propositional extensionality}}}}
-\put(4951,-5686){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(needs Prop-impredicativity)}}}}
-\put(6001,-5911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}(Berardi)}}}}
-\put(1576,-5386){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Not excluded-middle}}}}
-\put(3376,-6586){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Decidability of equality on any A}}}}
-\put(3601,-7336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Axiom K on A}}}}
-\put(3601,-7636){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of reflexivity proofs for equality on A}}}}
-\put(3601,-7936){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Uniqueness of equality proofs on A}}}}
-\put(3601,-8536){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\familydefault}{\mddefault}{\updefault}Invariance by substitution of reflexivity proofs for equality on A}}}}
-\put(9001,-4336){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional extensionality}}}}
-\put(3601,-8236){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Injectivity of equality on Sigma-types on A}}}}
-\put(6451,-6436){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Proof-irrelevance}}}}
-\put(3151,-211){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Operator epsilon}}}}
-\put(3151,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}}
-\put(3151,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}indefinite description}}}}
-\put(3151,-2311){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Functional choice axiom}}}}
-\put(451,-811){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Constructive}}}}
-\put(451,-1036){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}definite description}}}}
-\put(451,-2911){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\rmdefault}{\bfdefault}{\updefault}Axiom of unique choice}}}}
-\end{picture}%
diff --git a/doc/faq/axioms.png b/doc/faq/axioms.png
deleted file mode 100644
index a86eed7f12..0000000000
--- a/doc/faq/axioms.png
+++ /dev/null