Remove non-DFSG contentsupstream/8.3.pl3+dfsg

1 files changed, 0 insertions, 137 deletions

diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig
deleted file mode 100644
index 78e44886..00000000
--- a/doc/faq/axioms.fig
+++ /dev/null
@@ -1,137 +0,0 @@
-#FIG 3.2
-Landscape
-Center
-Inches
-Letter  
-100.00
-Single
--2
-1200 2
-5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 7222.500 4725 3825 4425 4800 4200 6000
-	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 8925.000 3600 9075 3450 8925 3600 8775
-	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 8625.000 3600 8775 3450 8625 3600 8475
-	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8325.000 3600 8475 3450 8325 3600 8175
-	1 1 1.00 60.00 120.00
-	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8625.000 3600 8775 3450 8625 3600 8475
-	1 1 1.00 60.00 120.00
-	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8925.000 3600 9075 3450 8925 3600 8775
-	1 1 1.00 60.00 120.00
-	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 9225.000 3600 9375 3450 9225 3600 9075
-	1 1 1.00 60.00 120.00
-	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 6309.515 5767.724 4200 3825 3450 5550 3825 7200
-	1 1 1.00 60.00 120.00
-6 2025 300 7725 525
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 7725 525 2025 525
-4 0 0 50 -1 0 12 0.0000 4 180 5700 2025 450 The dependency graph of axioms in the Calculus of Inductive Constructions\001
--6
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 4200 6225 4200 7200
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 7725 3900 7200 6000
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 7200 6225 7200 7050
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
-	1 1 1.00 60.00 120.00
-	1 1 1.00 60.00 120.00
-	 5550 5625 5550 6000
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 4575 6000 6450 6000
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
-	1 1 1.00 60.00 120.00
-	1 1 1.00 60.00 120.00
-	 3375 3225 3375 3600
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 3373 1950 3376 2250
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
-	1 1 1.00 60.00 120.00
-	1 1 1.00 60.00 120.00
-	 3375 2625 3375 3000
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 2175 3600 3750 3600
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 3075 2475 2475 2475
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 3374 1125 3377 1425
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 1049 1950 1052 2250
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 1048 1125 1051 1425
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 3075 975 1575 975
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 3075 1725 2025 1725
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 4
-	 8025 5925 8250 5925 9000 4950 9150 4950
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 8625 5400 8250 3900
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 7050 7350 4575 7950
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 4200 7500 4200 7950
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 4714 6255 7039 7080
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 60.00 120.00
-	 1500 3900 2175 6000
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
-	1 1 1.00 60.00 120.00
-	1 1 1.00 60.00 120.00
-	 1139 2771 1364 3521
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 4425 4875 7350 3825
-3 0 0 1 0 7 50 -1 -1 0.000 0 0 0 4
-	 6450 7050 4050 6675 3750 6825 3750 7050
-	 0.000 1.000 1.000 0.000
-4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 3750 Predicate extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 3750 Relational choice axiom\001
-4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 6150 Propositional extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 180 1005 450 1050 Operator iota\001
-4 0 0 50 -1 2 12 0.0000 4 135 1020 450 1650 Constructive\001
-4 0 0 50 -1 2 12 0.0000 4 180 1530 450 1875 definite description\001
-4 0 0 50 -1 2 12 0.0000 4 180 2010 9000 5175 Functional extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 180 4740 150 10050 Statements in boldface are the most "interesting" ones for Coq\001
-4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 8475 Uniqueness of reflexivity proofs for equality on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 8775 Uniqueness of equality proofs on A\001
-4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 8175 Axiom K on A\001
-4 0 0 50 -1 2 12 0.0000 4 135 1455 6450 7275 Proof-irrelevance\001
-4 0 0 50 -1 2 12 0.0000 4 180 3360 3600 9075 Injectivity of equality on Sigma-types on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 2175 4950 6525 (needs Prop-impredicativity)\001
-4 0 0 50 -1 0 12 0.0000 4 180 705 6000 6750 (Berardi)\001
-4 0 0 50 -1 2 12 0.0000 4 135 1290 3675 6225 Excluded-middle\001
-4 0 0 50 -1 0 12 0.0000 4 180 1905 4950 5550 Propositional degeneracy\001
-4 0 0 50 -1 0 12 0.0000 4 180 1050 3750 5250 (Diaconescu)\001
-4 0 0 50 -1 0 12 0.0000 4 180 2475 3375 7425 Decidability of equality on any A\001
-4 0 0 50 -1 0 12 0.0000 4 180 1620 1275 5025 (if Set impredicative)\001
-4 0 0 50 -1 0 12 0.0000 4 135 1560 1575 6225 Not excluded-middle\001
-4 0 0 50 -1 0 12 0.0000 4 180 1770 450 2625 in propositional context\001
-4 0 0 50 -1 2 12 0.0000 4 135 1020 3150 1650 Constructive\001
-4 0 0 50 -1 2 12 0.0000 4 180 1665 3150 1875 indefinite description\001
-4 0 0 50 -1 0 12 0.0000 4 180 2610 3150 2400 Constructive indefinite description\001
-4 0 0 50 -1 0 12 0.0000 4 180 1770 3150 2625 in propositional context\001
-4 0 0 50 -1 2 12 0.0000 4 135 1935 3150 3150 Functional choice axiom\001
-4 0 0 50 -1 0 12 0.0000 4 135 2100 450 2400 Constructive definite descr.\001
-4 0 0 50 -1 2 12 0.0000 4 180 1845 450 3750 Axiom of unique choice\001
-4 0 0 50 -1 2 12 0.0000 4 180 1365 3150 1050 Operator epsilon\001