aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build2
-rw-r--r--dev/vm_printers.ml1
-rw-r--r--doc/faq/FAQ.tex35
-rw-r--r--doc/faq/axioms.eps413
-rw-r--r--doc/faq/axioms.eps_t43
-rw-r--r--doc/faq/axioms.fig100
-rw-r--r--doc/faq/axioms.pdfbin0 -> 4974 bytes
-rw-r--r--doc/faq/axioms.pdf_t43
-rw-r--r--doc/faq/axioms.pngbin10075 -> 32222 bytes
-rw-r--r--doc/refman/RefMan-ext.tex3
-rw-r--r--doc/refman/RefMan-pro.tex7
-rw-r--r--kernel/cbytecodes.ml29
-rw-r--r--kernel/cbytecodes.mli28
-rw-r--r--kernel/cemitcodes.ml1
-rw-r--r--parsing/g_xml.ml4290
-rw-r--r--plugins/extraction/extraction.ml3
-rw-r--r--pretyping/miscops.ml2
-rw-r--r--printing/printmod.ml10
-rw-r--r--test-suite/bugs/closed/3743.v11
-rw-r--r--test-suite/output/PrintModule.out4
-rw-r--r--test-suite/output/PrintModule.v34
-rw-r--r--test-suite/success/primitiveproj.v7
-rw-r--r--tools/coqdep.ml31
-rw-r--r--tools/coqdep_common.ml91
-rw-r--r--tools/coqdep_common.mli6
25 files changed, 560 insertions, 634 deletions
diff --git a/Makefile.build b/Makefile.build
index 6650427e6..842399efd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -101,7 +101,7 @@ BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
-ifeq ($(shell which codesign 2>&1 > /dev/null && echo $(ARCH)),Darwin)
+ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist"
CODESIGN:=codesign -s -
else
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 4578a3b33..3d688011c 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -49,6 +49,7 @@ let rec ppzipper z =
close_box()
| Zfix _ -> print_string "Zfix"
| Zswitch _ -> print_string "Zswitch"
+ | Zproj _ -> print_string "Zproj"
and ppstack s =
open_hovbox 0;
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 589933578..8495156ca 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -503,19 +503,34 @@ $\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$
\item Extensionality of functions: $\forall f g:A\rightarrow B, (\forall x, f(x)=g(x)) \rightarrow f=g$
\end{itemize}
-Here is a summary of the relative strength of these axioms, most
-proofs can be found in directory {\tt Logic} of the standard library.
-The justification of their validity relies on the interpretability in
-set theory.
-
+Figure~\ref{fig:axioms} is a summary of the relative strength of these
+axioms, most proofs can be found in directory {\tt Logic} of the standard
+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
-\includegraphics[width=1.0\textwidth]{axioms.png}
+\scalebox{0.65}{\input{axioms.pdf_t}}
+%\includegraphics[width=1.0\textwidth]{axioms.png}
\else
-\includegraphics[width=1.0\textwidth]{axioms.eps}
+\scalebox{0.65}{\input{axioms.eps_t}}
+%\includegraphics[width=1.0\textwidth]{axioms.eps}
\fi
+\end{center}
%END LATEX
+\caption{The dependency graph of axioms in the Calculus of Inductive Constructions}
+\label{fig:axioms}
+\end{figure}
\Question{What standard axioms are inconsistent with {\Coq}?}
@@ -2579,12 +2594,6 @@ Qed.
You can help {\Coq} using the {\pattern} tactic.
-\Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?}
-
- This is because \texttt{\{x:A|P x\}} is a notation for
-\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to
-$\eta$-conversion, this is different from \texttt{sig P}.
-
\Question{I copy-paste a term and {\Coq} says it is not convertible
to the original term. Sometimes it even says the copied term is not
diff --git a/doc/faq/axioms.eps b/doc/faq/axioms.eps
index 3f3c01c43..836afc347 100644
--- a/doc/faq/axioms.eps
+++ b/doc/faq/axioms.eps
@@ -1,11 +1,11 @@
-%!PS-Adobe-2.0 EPSF-2.0
+%!PS-Adobe-3.0 EPSF-3.0
%%Title: axioms.fig
-%%Creator: fig2dev Version 3.2 Patchlevel 4
-%%CreationDate: Wed May 5 18:30:03 2004
-%%For: herbelin@limoux.polytechnique.fr (Hugo Herbelin)
-%%BoundingBox: 0 0 437 372
-%%Magnification: 1.0000
+%%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
@@ -44,10 +44,6 @@ $F2psDict /mtrx matrix put
/col31 {1.000 0.840 0.000 srgb} bind def
end
-save
-newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpath
--90.0 435.2 translate
-1 -1 scale
/cp {closepath} bind def
/ef {eofill} bind def
@@ -80,51 +76,25 @@ newpath 0 372 moveto 0 0 lineto 437 0 lineto 437 372 lineto closepath clip newpa
bind def
/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul
4 -2 roll mul srgb} bind def
-/reencdict 12 dict def /ReEncode { reencdict begin
-/newcodesandnames exch def /newfontname exch def /basefontname exch def
-/basefontdict basefontname findfont def /newfont basefontdict maxlength dict def
-basefontdict { exch dup /FID ne { dup /Encoding eq
-{ exch dup length array copy newfont 3 1 roll put }
-{ exch newfont 3 1 roll put } ifelse } { pop pop } ifelse } forall
-newfont /FontName newfontname put newcodesandnames aload pop
-128 1 255 { newfont /Encoding get exch /.notdef put } for
-newcodesandnames length 2 idiv { newfont /Encoding get 3 1 roll put } repeat
-newfontname newfont definefont pop end } def
-/isovec [
-8#055 /minus 8#200 /grave 8#201 /acute 8#202 /circumflex 8#203 /tilde
-8#204 /macron 8#205 /breve 8#206 /dotaccent 8#207 /dieresis
-8#210 /ring 8#211 /cedilla 8#212 /hungarumlaut 8#213 /ogonek 8#214 /caron
-8#220 /dotlessi 8#230 /oe 8#231 /OE
-8#240 /space 8#241 /exclamdown 8#242 /cent 8#243 /sterling
-8#244 /currency 8#245 /yen 8#246 /brokenbar 8#247 /section 8#250 /dieresis
-8#251 /copyright 8#252 /ordfeminine 8#253 /guillemotleft 8#254 /logicalnot
-8#255 /hyphen 8#256 /registered 8#257 /macron 8#260 /degree 8#261 /plusminus
-8#262 /twosuperior 8#263 /threesuperior 8#264 /acute 8#265 /mu 8#266 /paragraph
-8#267 /periodcentered 8#270 /cedilla 8#271 /onesuperior 8#272 /ordmasculine
-8#273 /guillemotright 8#274 /onequarter 8#275 /onehalf
-8#276 /threequarters 8#277 /questiondown 8#300 /Agrave 8#301 /Aacute
-8#302 /Acircumflex 8#303 /Atilde 8#304 /Adieresis 8#305 /Aring
-8#306 /AE 8#307 /Ccedilla 8#310 /Egrave 8#311 /Eacute
-8#312 /Ecircumflex 8#313 /Edieresis 8#314 /Igrave 8#315 /Iacute
-8#316 /Icircumflex 8#317 /Idieresis 8#320 /Eth 8#321 /Ntilde 8#322 /Ograve
-8#323 /Oacute 8#324 /Ocircumflex 8#325 /Otilde 8#326 /Odieresis 8#327 /multiply
-8#330 /Oslash 8#331 /Ugrave 8#332 /Uacute 8#333 /Ucircumflex
-8#334 /Udieresis 8#335 /Yacute 8#336 /Thorn 8#337 /germandbls 8#340 /agrave
-8#341 /aacute 8#342 /acircumflex 8#343 /atilde 8#344 /adieresis 8#345 /aring
-8#346 /ae 8#347 /ccedilla 8#350 /egrave 8#351 /eacute
-8#352 /ecircumflex 8#353 /edieresis 8#354 /igrave 8#355 /iacute
-8#356 /icircumflex 8#357 /idieresis 8#360 /eth 8#361 /ntilde 8#362 /ograve
-8#363 /oacute 8#364 /ocircumflex 8#365 /otilde 8#366 /odieresis 8#367 /divide
-8#370 /oslash 8#371 /ugrave 8#372 /uacute 8#373 /ucircumflex
-8#374 /udieresis 8#375 /yacute 8#376 /thorn 8#377 /ydieresis] def
-/Times-Roman /Times-Roman-iso isovec ReEncode
/$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
%
@@ -132,247 +102,316 @@ $F2psBegin
% here starts figure with depth 50
% Arc
7.500 slw
+0 slc
gs clippath
-3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
+4188 5861 m 4168 6010 l 4227 6018 l 4247 5869 l 4247 5869 l 4202 5984 l 4188 5861 l cp
eoclip
-n 3600.0 6750.0 150.0 90.0 -90.0 arc
+n 14032.5 7222.5 9908.2 -159.9465 -172.9126 arcn
gs col0 s gr
gr
% arrowhead
-n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l cp gs 0.00 setgray ef gr col0 s
+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
-3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 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 6450.0 150.0 90.0 -90.0 arc
+n 3600.0 8925.0 150.0 90.0000 -90.0000 arc
gs col0 s gr
gr
% arrowhead
-n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l cp gs 0.00 setgray ef gr col0 s
+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
-3626 6020 m 3599 5966 l 3465 6034 l 3586 6007 l 3492 6087 l cp
-3599 6333 m 3626 6279 l 3492 6212 l 3586 6293 l 3465 6265 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 6150.0 150.0 90.0 -90.0 arc
+n 3600.0 8625.0 150.0 90.0000 -90.0000 arc
gs col0 s gr
gr
% arrowhead
-n 3492 6087 m 3586 6007 l 3465 6034 l 3492 6087 l cp gs 0.00 setgray ef gr col0 s
+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 6265 m 3586 6293 l 3492 6212 l 3465 6265 l cp gs 0.00 setgray ef gr col0 s
+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
-3626 6320 m 3599 6266 l 3465 6334 l 3586 6307 l 3492 6387 l cp
-3599 6633 m 3626 6579 l 3492 6512 l 3586 6593 l 3465 6565 l cp
+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 6450.0 150.0 90.0 -90.0 arc
+n 3600.0 8625.0 150.0 90.0000 -90.0000 arc
gs col0 s gr
gr
% arrowhead
-n 3492 6387 m 3586 6307 l 3465 6334 l 3492 6387 l cp gs 0.00 setgray ef gr col0 s
+n 3465 8740 m 3586 8768 l 3492 8687 l 3465 8740 l cp gs 0.00 setgray ef gr col0 s
% arrowhead
-n 3465 6565 m 3586 6593 l 3492 6512 l 3465 6565 l cp gs 0.00 setgray ef gr col0 s
+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
-3626 6620 m 3599 6566 l 3465 6634 l 3586 6607 l 3492 6687 l cp
-3599 6933 m 3626 6879 l 3492 6812 l 3586 6893 l 3465 6865 l cp
+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 6750.0 150.0 90.0 -90.0 arc
+n 3600.0 8925.0 150.0 90.0000 -90.0000 arc
gs col0 s gr
gr
% arrowhead
-n 3492 6687 m 3586 6607 l 3465 6634 l 3492 6687 l cp gs 0.00 setgray ef gr col0 s
+n 3465 9040 m 3586 9068 l 3492 8987 l 3465 9040 l cp gs 0.00 setgray ef gr col0 s
% arrowhead
-n 3465 6865 m 3586 6893 l 3492 6812 l 3465 6865 l cp gs 0.00 setgray ef gr col0 s
+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
-3626 6920 m 3599 6866 l 3465 6934 l 3586 6907 l 3492 6987 l cp
-3599 7233 m 3626 7179 l 3492 7112 l 3586 7193 l 3465 7165 l cp
+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 7050.0 150.0 90.0 -90.0 arc
+n 3600.0 9225.0 150.0 90.0000 -90.0000 arc
gs col0 s gr
gr
% arrowhead
-n 3492 6987 m 3586 6907 l 3465 6934 l 3492 6987 l cp gs 0.00 setgray ef gr col0 s
+n 3465 9340 m 3586 9368 l 3492 9287 l 3465 9340 l cp gs 0.00 setgray ef gr col0 s
% arrowhead
-n 3465 7165 m 3586 7193 l 3492 7112 l 3465 7165 l cp gs 0.00 setgray ef gr col0 s
+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
-4168 4060 m 4227 4068 l 4247 3919 l 4202 4034 l 4188 3911 l cp
+3733 7095 m 3805 7227 l 3858 7198 l 3785 7066 l 3785 7066 l 3817 7186 l 3733 7095 l cp
eoclip
-n 14032.5 5272.5 9908.2 -159.9 -172.9 arcn
+n 6309.5 5767.7 2867.8 -137.3570 150.0374 arcn
gs col0 s gr
gr
% arrowhead
-n 4188 3911 m 4202 4034 l 4247 3919 l 4188 3911 l cp gs 0.00 setgray ef gr col0 s
+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
-4170 5790 m 4230 5790 l 4230 5639 l 4200 5759 l 4170 5639 l cp
+7170 6914 m 7170 7065 l 7230 7065 l 7230 6914 l 7230 6914 l 7200 7034 l 7170 6914 l cp
eoclip
-n 4200 5175 m
- 4200 5775 l gs col0 s gr gr
+n 7200 6225 m
+ 7200 7050 l gs col0 s gr gr
% arrowhead
-n 4170 5639 m 4200 5759 l 4230 5639 l 4170 5639 l cp gs 0.00 setgray ef gr col0 s
+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
-4553 5749 m 4567 5807 l 4714 5771 l 4591 5771 l 4700 5713 l cp
+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 7050 5175 m
- 4575 5775 l gs col0 s gr gr
+n 5550 5625 m
+ 5550 6000 l gs col0 s gr gr
% arrowhead
-n 4700 5713 m 4591 5771 l 4714 5771 l 4700 5713 l cp gs 0.00 setgray ef gr col0 s
+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
-4170 4890 m 4230 4890 l 4230 4739 l 4200 4859 l 4170 4739 l cp
+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 4200 4275 m
- 4200 4875 l gs col0 s gr gr
+n 3375 3225 m
+ 3375 3600 l gs col0 s gr gr
% arrowhead
-n 4170 4739 m 4200 4859 l 4230 4739 l 4170 4739 l cp gs 0.00 setgray ef gr col0 s
+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
-7131 4907 m 7147 4850 l 7001 4810 l 7109 4871 l 6985 4868 l cp
+3344 2114 m 3346 2265 l 3406 2264 l 3404 2113 l 3404 2113 l 3376 2234 l 3344 2114 l cp
eoclip
-n 4950 4275 m
- 7125 4875 l gs col0 s gr gr
+n 3373 1950 m
+ 3376 2250 l gs col0 s gr gr
% arrowhead
-n 6985 4868 m 7109 4871 l 7001 4810 l 6985 4868 l cp gs 0.00 setgray ef gr col0 s
+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
-7167 4057 m 7225 4071 l 7262 3924 l 7204 4034 l 7204 3910 l cp
+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 7725 1950 m
- 7200 4050 l gs col0 s gr gr
+n 3375 2625 m
+ 3375 3000 l gs col0 s gr gr
% arrowhead
-n 7204 3910 m 7204 4034 l 7262 3924 l 7204 3910 l cp gs 0.00 setgray ef gr col0 s
+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 4350 3075 m
- 7350 1950 l gs col0 s gr
+n 2175 3600 m
+ 3750 3600 l gs col0 s gr
% Polyline
gs clippath
-7170 4890 m 7230 4890 l 7230 4739 l 7200 4859 l 7170 4739 l cp
+2611 2445 m 2460 2445 l 2460 2505 l 2611 2505 l 2611 2505 l 2491 2475 l 2611 2445 l cp
eoclip
-n 7200 4275 m
- 7200 4875 l gs col0 s gr gr
+n 3075 2475 m
+ 2475 2475 l gs col0 s gr gr
% arrowhead
-n 7170 4739 m 7200 4859 l 7230 4739 l 7170 4739 l cp gs 0.00 setgray ef gr col0 s
+n 2611 2445 m 2491 2475 l 2611 2505 l 2611 2445 l cp gs 0.00 setgray ef gr col0 s
% Polyline
-n 3075 1875 m
- 3975 1875 l gs col0 s gr
+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
-5520 4065 m 5580 4065 l 5580 3914 l 5550 4034 l 5520 3914 l cp
-5580 3660 m 5520 3660 l 5520 3811 l 5550 3691 l 5580 3811 l cp
+1711 945 m 1560 945 l 1560 1005 l 1711 1005 l 1711 1005 l 1591 975 l 1711 945 l cp
eoclip
-n 5550 3675 m
- 5550 4050 l gs col0 s gr gr
+n 3075 975 m
+ 1575 975 l gs col0 s gr gr
% arrowhead
-n 5580 3811 m 5550 3691 l 5520 3811 l 5580 3811 l cp gs 0.00 setgray ef gr col0 s
+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 5520 3914 m 5550 4034 l 5580 3914 l 5520 3914 l cp gs 0.00 setgray ef gr col0 s
+n 2161 1695 m 2041 1725 l 2161 1755 l 2161 1695 l cp gs 0.00 setgray ef gr col0 s
% Polyline
-n 4575 4050 m
- 6450 4050 l gs col0 s gr
+n 8025 5925 m 8250 5925 l 9000 4950 l
+ 9150 4950 l gs col0 s gr
% Polyline
gs clippath
-3495 2265 m 3555 2265 l 3555 2114 l 3525 2234 l 3495 2114 l cp
-3555 1860 m 3495 1860 l 3495 2011 l 3525 1891 l 3555 2011 l cp
+8312 4025 m 8275 3878 l 8217 3892 l 8254 4039 l 8254 4039 l 8254 3916 l 8312 4025 l cp
eoclip
-n 3525 1875 m
- 3525 2250 l gs col0 s gr gr
+n 8625 5400 m
+ 8250 3900 l gs col0 s gr gr
% arrowhead
-n 3555 2011 m 3525 1891 l 3495 2011 l 3555 2011 l cp gs 0.00 setgray ef gr col0 s
+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 3495 2114 m 3525 2234 l 3555 2114 l 3495 2114 l cp gs 0.00 setgray ef gr col0 s
+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
-2219 3988 m 2279 3991 l 2285 3840 l 2251 3959 l 2225 3838 l cp
+4170 7814 m 4170 7965 l 4230 7965 l 4230 7814 l 4230 7814 l 4200 7934 l 4170 7814 l cp
eoclip
-n 2325 1875 m
- 2250 3975 l gs col0 s gr gr
+n 4200 7500 m
+ 4200 7950 l gs col0 s gr gr
% arrowhead
-n 2225 3838 m 2251 3959 l 2285 3840 l 2225 3838 l cp gs 0.00 setgray ef gr col0 s
+n 4170 7814 m 4200 7934 l 4230 7814 l 4170 7814 l cp gs 0.00 setgray ef gr col0 s
% Polyline
-n 7800 1275 m
- 2100 1275 l gs col0 s gr
-/Times-Roman-iso ff 180.00 scf sf
-6600 5100 m
-gs 1 -1 sc (Proof-irrelevance) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3675 4200 m
-gs 1 -1 sc (Excluded-middle) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-6900 1800 m
-gs 1 -1 sc (Predicate extensionality) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3375 3525 m
-gs 1 -1 sc (\(Diaconescu\)) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-4650 3600 m
-gs 1 -1 sc (Propositional degeneracy) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3825 1800 m
-gs 1 -1 sc (Relational choice axiom) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-1725 1800 m
-gs 1 -1 sc (Description principle) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-2550 2400 m
-gs 1 -1 sc (Functional choice axiom) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 5100 m
-gs 1 -1 sc (Decidability of equality on $A$) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-4425 4575 m
-gs 1 -1 sc (\(needs Prop-impredicativity\)) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-5025 4725 m
-gs 1 -1 sc (\(Berardi\)) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-1500 3075 m
-gs 1 -1 sc (\(if Set impredicative\)) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-1500 4200 m
-gs 1 -1 sc (Not excluded-middle) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 6000 m
-gs 1 -1 sc (Axiom K on A) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 7200 m
-gs 1 -1 sc (Invariance by substitution of reflexivity proofs for equality on A) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-6150 4200 m
-gs 1 -1 sc (Propositional extensionality) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-2100 1200 m
-gs 1 -1 sc (The dependency graph of axioms in the Calculus of Inductive Constructions) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 6900 m
-gs 1 -1 sc (Injectivity of equality on sigma-types on A) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 6300 m
-gs 1 -1 sc (Uniqueness of reflexivity proofs for equality on A) col0 sh gr
-/Times-Roman-iso ff 180.00 scf sf
-3600 6600 m
-gs 1 -1 sc (Uniqueness of equality proofs on A) col0 sh gr
+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;
-$F2psEnd
-rs
+pagefooter
showpage
+%%Trailer
+%EOF
diff --git a/doc/faq/axioms.eps_t b/doc/faq/axioms.eps_t
new file mode 100644
index 000000000..38f1a3fed
--- /dev/null
+++ b/doc/faq/axioms.eps_t
@@ -0,0 +1,43 @@
+\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.fig b/doc/faq/axioms.fig
index 78e448865..963178503 100644
--- a/doc/faq/axioms.fig
+++ b/doc/faq/axioms.fig
@@ -1,4 +1,4 @@
-#FIG 3.2
+#FIG 3.2 Produced by xfig version 3.2.5c
Landscape
Center
Inches
@@ -27,14 +27,6 @@ Single
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
@@ -45,8 +37,6 @@ Single
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
@@ -68,12 +58,6 @@ Single
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
@@ -89,49 +73,59 @@ Single
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 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
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
+ 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
+ 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
1500 3900 2175 6000
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
+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 0 2
1 1 1.00 60.00 120.00
+ 4714 6255 7039 7080
+2 1 0 1 -1 7 50 -1 -1 0.000 0 0 -1 1 0 2
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
+ 4200 6225 4200 7200
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
+4 0 -1 50 -1 2 12 0.0000 2 135 1440 3675 6225 Excluded-middle\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1065 450 1050 Operator iota\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2850 3150 2400 Constructive indefinite description\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1965 3150 2625 in propositional context\001
+4 0 -1 50 -1 0 12 0.0000 2 135 2235 450 2400 Constructive definite descr.\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1965 450 2625 in propositional context\001
+4 0 -1 50 -1 0 12 0.0000 2 135 1995 3825 3750 Relational choice axiom\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1965 6900 3750 Predicate extensionality\001
+4 0 -1 50 -1 0 12 0.0000 2 180 1710 1275 5025 (if Set impredicative)\001
+4 0 -1 50 -1 0 12 0.0000 2 165 1065 3750 5250 (Diaconescu)\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2070 4950 5550 Propositional degeneracy\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2310 6150 6150 Propositional extensionality\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2325 4950 6525 (needs Prop-impredicativity)\001
+4 0 -1 50 -1 0 12 0.0000 2 165 720 6000 6750 (Berardi)\001
+4 0 -1 50 -1 0 12 0.0000 2 135 1725 1575 6225 Not excluded-middle\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2730 3375 7425 Decidability of equality on any A\001
+4 0 -1 50 -1 0 12 0.0000 2 135 1170 3600 8175 Axiom K on A\001
+4 0 -1 50 -1 0 12 0.0000 2 180 4035 3600 8475 Uniqueness of reflexivity proofs for equality on A\001
+4 0 -1 50 -1 0 12 0.0000 2 180 2865 3600 8775 Uniqueness of equality proofs on A\001
+4 0 -1 50 -1 0 12 0.0000 2 180 5220 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001
+4 0 -1 50 -1 2 12 0.0000 2 180 2145 9000 5175 Functional extensionality\001
+4 0 -1 50 -1 2 12 0.0000 2 180 3585 3600 9075 Injectivity of equality on Sigma-types on A\001
+4 0 -1 50 -1 2 12 0.0000 2 135 1515 6450 7275 Proof-irrelevance\001
+4 0 -1 50 -1 2 12 0.0000 2 180 1440 3150 1050 Operator epsilon\001
+4 0 -1 50 -1 2 12 0.0000 2 135 1080 3150 1650 Constructive\001
+4 0 -1 50 -1 2 12 0.0000 2 180 1785 3150 1875 indefinite description\001
+4 0 -1 50 -1 2 12 0.0000 2 135 2085 3150 3150 Functional choice axiom\001
+4 0 -1 50 -1 2 12 0.0000 2 135 1080 450 1650 Constructive\001
+4 0 -1 50 -1 2 12 0.0000 2 180 1620 450 1875 definite description\001
+4 0 -1 50 -1 2 12 0.0000 2 180 1980 450 3750 Axiom of unique choice\001
diff --git a/doc/faq/axioms.pdf b/doc/faq/axioms.pdf
new file mode 100644
index 000000000..2ba5bf85b
--- /dev/null
+++ b/doc/faq/axioms.pdf
Binary files differ
diff --git a/doc/faq/axioms.pdf_t b/doc/faq/axioms.pdf_t
new file mode 100644
index 000000000..06dc4b280
--- /dev/null
+++ b/doc/faq/axioms.pdf_t
@@ -0,0 +1,43 @@
+\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
index 2aee09166..a86eed7f1 100644
--- a/doc/faq/axioms.png
+++ b/doc/faq/axioms.png
Binary files differ
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index cc5239a77..d63d22a71 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1375,9 +1375,6 @@ Check (fun l => map length l = map (list nat) nat length l).
\Rem To know which are the implicit arguments of an object, use the command
{\tt Print Implicit} (see \ref{PrintImplicit}).
-\Rem If the list of arguments is empty, the command removes the
-implicit arguments of {\qualid}.
-
\subsection{Automatic declaration of implicit arguments for a constant}
{\Coq} can also automatically detect what are the implicit arguments
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 684a4add4..7af87a399 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -453,11 +453,16 @@ In the case of a non-product goal, it prints nothing.
This command is similar to the previous one, it simulates the naming
process of an {\tt Intros}.
-\item{\tt Show Existentials\label{ShowExistentials}}\comindex{Show Existentials}
+\item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
\\ It displays
the set of all uninstantiated existential variables in the current proof tree,
along with the type and the context of each variable.
+\item{\tt Show Universes.\label{ShowUniverses}}\comindex{Show Universes}
+\\ It displays the set of all universe constraints and its
+normalized form at the current stage of the proof, useful for
+debugging universe inconsistencies.
+
\end{Variants}
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 3271ac145..940b5528d 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -24,8 +24,8 @@ let fix_tag = 3
let switch_tag = 4
let cofix_tag = 5
let cofix_evaluated_tag = 6
-(* It could be greate if OCaml export this value,
- So fixme if this occur in a new version of OCaml *)
+(* It would be great if OCaml exported this value,
+ So fixme if this happens in a new version of OCaml *)
let last_variant_tag = 245
type structured_constant =
@@ -35,7 +35,6 @@ type structured_constant =
| Const_b0 of tag
| Const_bn of tag * structured_constant array
-
type reloc_table = (tag * int) array
type annot_switch =
@@ -59,24 +58,22 @@ type instruction =
| Kpush
| Kpop of int
| Kpush_retaddr of Label.t
- | Kapply of int (* number of arguments *)
- | Kappterm of int * int (* number of arguments, slot size *)
- | Kreturn of int (* slot size *)
+ | Kapply of int
+ | Kappterm of int * int
+ | Kreturn of int
| Kjump
| Krestart
- | Kgrab of int (* number of arguments *)
- | Kgrabrec of int (* rec arg *)
- | Kclosure of Label.t * int (* label, number of free variables *)
+ | Kgrab of int
+ | Kgrabrec of int
+ | Kclosure of Label.t * int
| Kclosurerec of int * int * Label.t array * Label.t array
- (* nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
- (* nb fv, init, lbl types, lbl bodies *)
| Kgetglobal of pconstant
| Kconst of structured_constant
- | Kmakeblock of int * tag (* size, tag *)
+ | Kmakeblock of int * tag
| Kmakeprod
| Kmakeswitchblock of Label.t * Label.t * annot_switch * int
- | Kswitch of Label.t array * Label.t array (* consts,blocks *)
+ | Kswitch of Label.t array * Label.t array
| Kpushfields of int
| Kfield of int
| Ksetfield of int
@@ -210,7 +207,7 @@ let rec pp_instr i =
prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
str " bodies = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblb))
- | Kgetglobal (id,u) -> str "getglobal " ++ pr_con id
+ | Kgetglobal (id,_u) -> str "getglobal " ++ pr_con id
| Kconst sc ->
str "const " ++ pp_struct_const sc
| Kmakeblock(n, m) ->
@@ -261,12 +258,12 @@ and pp_bytecodes c =
match c with
| [] -> str ""
| Klabel lbl :: c ->
- str "L" ++ int lbl ++ str ":" ++ str "\n" ++
+ str "L" ++ int lbl ++ str ":" ++ fnl () ++
pp_bytecodes c
| Ksequence (l1, l2) :: c ->
pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c
| i :: c ->
- str "\t" ++ pp_instr i ++ str "\n" ++ pp_bytecodes c
+ tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
let dump_bytecode c =
pperrnl (pp_bytecodes c);
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 745ef311b..8f594a45b 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -44,13 +44,13 @@ module Label :
type instruction =
| Klabel of Label.t
- | Kacc of int
- | Kenvacc of int
- | Koffsetclosure of int
- | Kpush
- | Kpop of int
- | Kpush_retaddr of Label.t
- | Kapply of int (** number of arguments *)
+ | Kacc of int (** accu = sp[n] *)
+ | Kenvacc of int (** accu = coq_env[n] *)
+ | Koffsetclosure of int (** accu = &coq_env[n] *)
+ | Kpush (** sp = accu :: sp *)
+ | Kpop of int (** sp = skipn n sp *)
+ | Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *)
+ | Kapply of int (** number of arguments (arguments on top of stack) *)
| Kappterm of int * int (** number of arguments, slot size *)
| Kreturn of int (** slot size *)
| Kjump
@@ -62,15 +62,15 @@ type instruction =
(** nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
(** nb fv, init, lbl types, lbl bodies *)
- | Kgetglobal of pconstant
+ | Kgetglobal of pconstant (** accu = coq_global_data[c] *)
| Kconst of structured_constant
- | Kmakeblock of int * tag (** size, tag *)
+ | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block *)
| Kmakeprod
| Kmakeswitchblock of Label.t * Label.t * annot_switch * int
| Kswitch of Label.t array * Label.t array (** consts,blocks *)
| Kpushfields of int
- | Kfield of int
- | Ksetfield of int
+ | Kfield of int (** accu = accu[n] *)
+ | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *)
| Kstop
| Ksequence of bytecodes * bytecodes
| Kproj of int * Constant.t (** index of the projected argument,
@@ -136,9 +136,9 @@ type vm_env = {
type comp_env = {
- nb_stack : int; (** nbre de variables sur la pile *)
- in_stack : int list; (** position dans la pile *)
- nb_rec : int; (** nbre de fonctions mutuellement *)
+ nb_stack : int; (** number of variables on the stack *)
+ in_stack : int list; (** position in the stack *)
+ nb_rec : int; (** number of mutually recursive functions *)
(** recursives = nbr *)
pos_rec : instruction list; (** instruction d'acces pour les variables *)
(** de point fix ou de cofix *)
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 0d9334a50..6dbfbe9cc 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -308,6 +308,7 @@ type to_patch = emitcodes * (patch list) * fv
let rec subst_strcst s sc =
match sc with
| Const_sorts _ | Const_b0 _ -> sc
+ | Const_proj p -> Const_proj (subst_constant s p)
| Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
| Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
deleted file mode 100644
index 992f9c59a..000000000
--- a/parsing/g_xml.ml4
+++ /dev/null
@@ -1,290 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Compat
-open Pp
-open Errors
-open Util
-open Names
-open Pcoq
-open Glob_term
-open Tacexpr
-open Libnames
-open Globnames
-open Detyping
-open Misctypes
-open Decl_kinds
-open Genredexpr
-open Tok (* necessary for camlp4 *)
-
-(* Generic xml parser without raw data *)
-
-type attribute = string * (Loc.t * string)
-type xml = XmlTag of Loc.t * string * attribute list * xml list
-
-let check_tags loc otag ctag =
- if not (String.equal otag ctag) then
- user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
- str "does not match open xml tag " ++ str otag ++ str ".")
-
-let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry)
-
-GEXTEND Gram
- GLOBAL: xml_eoi;
-
- xml_eoi:
- [ [ x = xml; EOI -> x ] ]
- ;
- xml:
- [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml;
- "<"; "/"; ctag = IDENT; ">" ->
- check_tags (!@loc) otag ctag;
- XmlTag (!@loc,ctag,attrs,l)
- | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" ->
- XmlTag (!@loc,tag,attrs,[])
- ] ]
- ;
- attr:
- [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ]
- ;
-END
-
-(* Errors *)
-
-let error_bad_arity loc n =
- let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in
- user_err_loc (loc,"",str "wrong number of arguments (expect " ++ str s ++ str ").")
-
-(* Interpreting attributes *)
-
-let nmtoken (loc,a) =
- try int_of_string a
- with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
-
-let get_xml_attr s al =
- try String.List.assoc s al
- with Not_found -> error ("No attribute "^s)
-
-(* Interpreting specific attributes *)
-
-let ident_of_cdata (loc,a) = Id.of_string a
-
-let uri_of_data s =
- try
- let n = String.index s ':' in
- let p = String.index s '.' in
- let s = String.sub s (n+2) (p-n-2) in
- for i = 0 to String.length s - 1 do
- match s.[i] with
- | '/' -> s.[i] <- '.'
- | _ -> ()
- done;
- qualid_of_string s
- with Not_found | Invalid_argument _ ->
- error ("Malformed URI \""^s^"\"")
-
-let constant_of_cdata (loc,a) =
- let q = uri_of_data a in
- try Nametab.locate_constant q
- with Not_found -> error ("No such constant "^string_of_qualid q)
-
-let global_of_cdata (loc,a) =
- let q = uri_of_data a in
- try Nametab.locate q
- with Not_found -> error ("No such global "^string_of_qualid q)
-
-let inductive_of_cdata a = match global_of_cdata a with
- | IndRef (kn,_) -> kn
- | _ -> error (string_of_qualid (uri_of_data (snd a)) ^" is not an inductive")
-
-let ltacref_of_cdata (loc,a) =
- let q = uri_of_data a in
- try (loc,Nametab.locate_tactic q)
- with Not_found -> error ("No such ltac "^string_of_qualid q)
-
-let sort_of_cdata (loc,a) = match a with
- | "Prop" -> GProp
- | "Set" -> GSet
- | "Type" -> GType None
- | _ -> user_err_loc (loc,"",str "sort expected.")
-
-let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
-
-let get_xml_inductive_kn al =
- inductive_of_cdata (* uriType apparent synonym of uri *)
- (try get_xml_attr "uri" al
- with UserError _ -> get_xml_attr "uriType" al)
-
-let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
-
-let get_xml_inductive al =
- (get_xml_inductive_kn al, nmtoken (get_xml_attr "noType" al))
-
-let get_xml_constructor al =
- (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al))
-
-let get_xml_binder al =
- try Name (ident_of_cdata (String.List.assoc "binder" al))
- with Not_found -> Anonymous
-
-let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
-
-let get_xml_name al = ident_of_cdata (get_xml_attr "name" al)
-
-let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
-
-let get_xml_no al = Evar.unsafe_of_int (nmtoken (get_xml_attr "no" al))
-
-(* A leak in the xml dtd: arities of constructor need to know global env *)
-
-let compute_branches_lengths ind =
- let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
- mip.Declarations.mind_consnrealdecls
-
-let compute_inductive_ndecls ind =
- Inductiveops.inductive_nrealdecls ind
-
-(* Interpreting constr as a glob_constr *)
-
-let rec interp_xml_constr = function
- | XmlTag (loc,"REL",al,[]) ->
- GVar (loc, get_xml_ident al)
- | XmlTag (loc,"VAR",al,[]) ->
- error "XML parser: unable to interp free variables"
- | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
- let body,decls = List.sep_last xl in
- let ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
- let body,decls = List.sep_last xl in
- let ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
- let body,defs = List.sep_last xl in
- let ctx = List.map interp_xml_def defs in
- List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b))
- ctx (interp_xml_target body)
- | XmlTag (loc,"APPLY",_,x::xl) ->
- GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
- | XmlTag (loc,"instantiate",_,
- (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
- GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
- | XmlTag (loc,"META",al,xl) ->
- GEvar (loc, get_xml_name al, Some (List.map interp_xml_substitution xl))
- | XmlTag (loc,"CONST",al,[]) ->
- GRef (loc, ConstRef (get_xml_constant al), None)
- | XmlTag (loc,"MUTCASE",al,x::y::yl) ->
- let ind = get_xml_inductive al in
- let p = interp_xml_patternsType x in
- let tm = interp_xml_inductiveTerm y in
- let vars = compute_branches_lengths ind in
- let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
- in
- let mat = simple_cases_matrix_of_branches ind brs in
- let n = compute_inductive_ndecls ind in
- let nal,rtn = return_type_of_predicate ind n p in
- GCases (loc,RegularStyle,rtn,[tm,nal],mat)
- | XmlTag (loc,"MUTIND",al,[]) ->
- GRef (loc, IndRef (get_xml_inductive al), None)
- | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
- GRef (loc, ConstructRef (get_xml_constructor al), None)
- | XmlTag (loc,"FIX",al,xl) ->
- let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
- let ln,lc,lt = List.split3 lnct in
- let lctx = List.map (fun _ -> []) ln in
- GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
- | XmlTag (loc,"COFIX",al,xl) ->
- let ln,lc,lt = List.split3 (List.map interp_xml_CoFixFunction xl) in
- GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
- | XmlTag (loc,"CAST",al,[x1;x2]) ->
- GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2))
- | XmlTag (loc,"SORT",al,[]) ->
- GSort (loc, get_xml_sort al)
- | XmlTag (loc,s,_,_) ->
- user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
-
-and interp_xml_tag s = function
- | XmlTag (loc,tag,al,xl) when String.equal tag s -> (loc,al,xl)
- | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "",
- str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
-
-and interp_xml_constr_alias s x =
- match interp_xml_tag s x with
- | (_,_,[x]) -> interp_xml_constr x
- | (loc,_,_) -> error_bad_arity loc 1
-
-and interp_xml_term x = interp_xml_constr_alias "term" x
-and interp_xml_type x = interp_xml_constr_alias "type" x
-and interp_xml_target x = interp_xml_constr_alias "target" x
-and interp_xml_body x = interp_xml_constr_alias "body" x
-and interp_xml_pattern x = interp_xml_constr_alias "pattern" x
-and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x
-and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x
-and interp_xml_arg x = interp_xml_constr_alias "arg" x
-and interp_xml_substitution x =
- match interp_xml_tag "substitution" x with
- _, al, [x] -> get_xml_name al, interp_xml_constr x
- | loc, _, _ -> error_bad_arity loc 1
- (* no support for empty substitution from official dtd *)
-
-and interp_xml_decl_alias s x =
- match interp_xml_tag s x with
- | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
- | (loc,_,_) -> error_bad_arity loc 1
-
-and interp_xml_def x = interp_xml_decl_alias "def" x
-and interp_xml_decl x = interp_xml_decl_alias "decl" x
-
-and interp_xml_recursionOrder x =
- let (loc, al, l) = interp_xml_tag "RecursionOrder" x in
- let (locs, s) = get_xml_attr "type" al in
- match s, l with
- | "Structural", [] -> GStructRec
- | "Structural", _ -> error_bad_arity loc 0
- | "WellFounded", [c] -> GWfRec (interp_xml_type c)
- | "WellFounded", _ -> error_bad_arity loc 1
- | "Measure", [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r))
- | "Measure", _ -> error_bad_arity loc 2
- | _ -> user_err_loc (locs,"",str "Invalid recursion order.")
-
-and interp_xml_FixFunction x =
- match interp_xml_tag "FixFunction" x with
- | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *)
- ((Some (nmtoken (get_xml_attr "recIndex" al)),
- interp_xml_recursionOrder x1),
- (get_xml_name al, interp_xml_type x2, interp_xml_body x3))
- | (loc,al,[x1;x2]) ->
- ((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec),
- (get_xml_name al, interp_xml_type x1, interp_xml_body x2))
- | (loc,_,_) ->
- error_bad_arity loc 1
-
-and interp_xml_CoFixFunction x =
- match interp_xml_tag "CoFixFunction" x with
- | (loc,al,[x1;x2]) ->
- (get_xml_name al, interp_xml_type x1, interp_xml_body x2)
- | (loc,_,_) ->
- error_bad_arity loc 1
-
-(* Interpreting tactic argument *)
-
-let rec interp_xml_tactic_arg = function
- | XmlTag (loc,"TERM",[],[x]) ->
- ConstrMayEval (ConstrTerm (interp_xml_constr x,None))
- | XmlTag (loc,"CALL",al,xl) ->
- let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in
- TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl)
- | XmlTag (loc,s,_,_) ->
- user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
-
-let parse_tactic_arg ch =
- interp_xml_tactic_arg
- (Pcoq.Gram.entry_parse xml_eoi
- (Pcoq.Gram.parsable (Stream.of_channel ch)))
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 080512b27..6ae519ef6 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -633,7 +633,8 @@ let rec extract_term env mle mlt c args =
| Construct (cp,u) ->
extract_cons_app env mle mlt cp u args
| Proj (p, c) ->
- extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args)
+ let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
+ extract_term env mle mlt term args
| Rel n ->
(* As soon as the expected [mlt] for the head is known, *)
(* we unify it with an fresh copy of the stored type of [Rel n]. *)
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index a2c97d2cb..0926e7a29 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,7 @@ let smartmap_cast_type f c =
let glob_sort_eq g1 g2 = match g1, g2 with
| GProp, GProp -> true
| GSet, GSet -> true
-| GType l1, GType l2 -> List.for_all2 CString.equal l1 l2
+| GType l1, GType l2 -> List.equal CString.equal l1 l2
| _ -> false
let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 295d8aaa6..a80bbb146 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -315,15 +315,17 @@ let rec print_typ_expr env mp locals mty =
let mapp = List.tl lapp in
hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
prlist_with_sep spc (print_modpath locals) mapp ++ str")")
- | MEwith(me,WithDef(idl,c))->
+ | MEwith(me,WithDef(idl,(c, _)))->
let env' = None in (* TODO: build a proper environment if env <> None *)
let s = String.concat "." (List.map Id.to_string idl) in
hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
- ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
- | MEwith(me,WithMod(idl,mp))->
+ ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
+ ++ Printer.pr_lconstr c)
+ | MEwith(me,WithMod(idl,mp'))->
let s = String.concat "." (List.map Id.to_string idl) in
hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++
- keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
+ keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
+ ++ print_modpath locals mp')
let print_mod_expr env mp locals = function
| MEident mp -> print_modpath locals mp
diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v
new file mode 100644
index 000000000..4dfb3380a
--- /dev/null
+++ b/test-suite/bugs/closed/3743.v
@@ -0,0 +1,11 @@
+(* File reduced by coq-bug-finder from original input, then from 967 lines to 469 lines, then from 459 lines to 35 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0
+ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *)
+Require Export Coq.Setoids.Setoid.
+
+Fail Add Parametric Relation A
+: A (@eq A)
+ transitivity proved by transitivity
+ as refine_rel.
+(* Toplevel input, characters 20-118:
+Anomaly: index to an anonymous variable. Please report. *) \ No newline at end of file
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
new file mode 100644
index 000000000..db464fd07
--- /dev/null
+++ b/test-suite/output/PrintModule.out
@@ -0,0 +1,4 @@
+Module N : S with Definition T := nat := M
+
+Module N : S with Module T := K := M
+
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
new file mode 100644
index 000000000..999d9a986
--- /dev/null
+++ b/test-suite/output/PrintModule.v
@@ -0,0 +1,34 @@
+Module FOO.
+
+Module M.
+ Definition T := nat.
+End M.
+
+Module Type S.
+ Parameter T : Set.
+End S.
+
+Module N : S with Definition T := nat := M.
+
+Print Module N.
+
+End FOO.
+
+Module BAR.
+
+Module K. End K.
+Module Type KS. End KS.
+
+Module M.
+ Module T := K.
+End M.
+
+Module Type S.
+ Declare Module T : KS.
+End S.
+
+Module N : S with Module T := K := M.
+
+Print Module N.
+
+End BAR.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 068f8ac3c..125615c53 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -188,3 +188,10 @@ Set Printing All.
Check (@p' nat).
Check p'.
Unset Printing All.
+
+Record wrap (A : Type) := { unwrap : A; unwrap2 : A }.
+
+Definition term (x : wrap nat) := x.(unwrap).
+Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
+Recursive Extraction term term'.
+(*Unset Printing Primitive Projection Parameters.*) \ No newline at end of file
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 397ccd8a2..be50b0e1c 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -37,14 +37,6 @@ let warning_mult suf iter =
in
iter check
-let add_coqlib_known recur phys_dir log_dir f =
- match get_extension f [".vo"] with
- | (basename,".vo") ->
- let name = log_dir@[basename] in
- let paths = if recur then suffixes name else [name] in
- List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
- | _ -> ()
-
let sort () =
let seen = Hashtbl.create 97 in
let rec loop file =
@@ -298,14 +290,21 @@ struct
module DAG = DAG(struct type t = string let compare = compare end)
(** TODO: we should share this code with Coqdep_common *)
+module VData = struct
+ type t = string list option * string list
+ let compare = Pervasives.compare
+end
+
+module VCache = Set.Make(VData)
+
let treat_coq_file chan =
let buf = Lexing.from_channel chan in
- let deja_vu_v = ref ([]: (string list option * string list) list)
- and deja_vu_ml = ref ([] : string list) in
+ let deja_vu_v = ref VCache.empty in
+ let deja_vu_ml = ref StrSet.empty in
let mark_v_done from acc str =
- let seen = List.mem (from, str) !deja_vu_v in
+ let seen = VCache.mem (from, str) !deja_vu_v in
if not seen then
- let () = addQueue deja_vu_v (from, str) in
+ let () = deja_vu_v := VCache.add (from, str) !deja_vu_v in
match search_v_known ?from str with
| None -> acc
| Some file_str -> (canonize file_str, !suffixe) :: acc
@@ -327,8 +326,8 @@ let treat_coq_file chan =
in
let decl acc str =
let s = basename_noext str in
- if not (List.mem s !deja_vu_ml) then
- let () = addQueue deja_vu_ml s in
+ if not (StrSet.mem s !deja_vu_ml) then
+ let () = deja_vu_ml := StrSet.add s !deja_vu_ml in
match search_mllib_known s with
| Some mldir -> (declare ".cma" mldir s) :: acc
| None ->
@@ -340,9 +339,9 @@ let treat_coq_file chan =
List.fold_left decl acc sl
| Load str ->
let str = Filename.basename str in
- let seen = List.mem (None, [str]) !deja_vu_v in
+ let seen = VCache.mem (None, [str]) !deja_vu_v in
if not seen then
- let () = addQueue deja_vu_v (None, [str]) in
+ let () = deja_vu_v := VCache.add (None, [str]) !deja_vu_v in
match search_v_known [str] with
| None -> acc
| Some file_str -> (canonize file_str, ".v") :: acc
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 879da6c58..967ec419f 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -18,6 +18,11 @@ open System
options (see for instance [option_natdynlk] below).
*)
+module StrSet = Set.Make(String)
+
+module StrList = struct type t = string list let compare = compare end
+module StrListMap = Map.Make(StrList)
+
let stderr = Pervasives.stderr
let stdout = Pervasives.stdout
@@ -27,7 +32,7 @@ let option_natdynlk = ref true
let option_boot = ref false
let option_mldep = ref None
-let norec_dirs = ref ([] : string list)
+let norec_dirs = ref StrSet.empty
let suffixe = ref ".vo"
@@ -76,11 +81,11 @@ let safe_hash_add cmp clq q (k, (v, b)) =
try
let (v2, _) = Hashtbl.find q k in
if not (cmp v v2) then
- let rec add_clash = function
- (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
- | cl::cltl -> cl::add_clash cltl
- | [] -> [(k,[v;v2])] in
- clq := add_clash !clq;
+ let nv =
+ try v :: StrListMap.find k !clq
+ with Not_found -> [v; v2]
+ in
+ clq := StrListMap.add k nv !clq;
(* overwrite previous bindings, as coqc does *)
Hashtbl.add q k (v, b)
with Not_found -> Hashtbl.add q k (v, b)
@@ -124,26 +129,33 @@ let get_prefix p l =
in
drop_prefix_rec (p, l)
-exception Found of string
-
-let search_v_known ?from s = match from with
-| None -> fst (Hashtbl.find vKnown s)
+let search_table (type r) is_root table ?from s = match from with
+| None -> Hashtbl.find table s
| Some from ->
- let iter logpath (phys_dir, root) =
- if root then match get_prefix from logpath with
+ let module M = struct exception Found of r end in
+ let iter logpath binding =
+ if is_root binding then match get_prefix from logpath with
| None -> ()
| Some rem ->
match get_prefix (List.rev s) (List.rev rem) with
| None -> ()
- | Some _ -> raise (Found phys_dir)
+ | Some _ -> raise (M.Found binding)
in
- try Hashtbl.iter iter vKnown; raise Not_found
- with Found s -> s
+ try Hashtbl.iter iter table; raise Not_found
+ with M.Found s -> s
let search_v_known ?from s =
- try Some (search_v_known ?from s) with Not_found -> None
+ let is_root (_, root) = root in
+ try
+ let (phys_dir, _) = search_table is_root vKnown ?from s in
+ Some phys_dir
+ with Not_found -> None
+
+let is_in_coqlib ?from s =
+ let is_root _ = true in
+ try search_table is_root coqlibKnown ?from s; true with Not_found -> false
-let clash_v = ref ([]: (string list * string list) list)
+let clash_v = ref (StrListMap.empty : string list StrListMap.t)
let error_cannot_parse s (i,j) =
Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
@@ -164,7 +176,7 @@ let warning_declare f s =
flush stderr
let warning_clash file dir =
- match List.assoc dir !clash_v with
+ match StrListMap.find dir !clash_v with
(f1::f2::fl) ->
let f = Filename.basename f1 in
let d1 = Filename.dirname f1 in
@@ -182,7 +194,7 @@ let warning_cannot_open_dir dir =
flush stderr
let safe_assoc from verbose file k =
- if verbose && List.mem_assoc k !clash_v then warning_clash file k;
+ if verbose && StrListMap.mem k !clash_v then warning_clash file k;
match search_v_known ?from k with
| None -> raise Not_found
| Some path -> path
@@ -240,16 +252,16 @@ let autotraite_fichier_ML md ext =
try
let chan = open_in (md ^ ext) in
let buf = Lexing.from_channel chan in
- let deja_vu = ref [md] in
+ let deja_vu = ref (StrSet.singleton md) in
let a_faire = ref "" in
let a_faire_opt = ref "" in
begin try
while true do
let (Use_module str) = caml_action buf in
- if List.mem str !deja_vu then
+ if StrSet.mem str !deja_vu then
()
else begin
- addQueue deja_vu str;
+ deja_vu := StrSet.add str !deja_vu;
let byte,opt = depend_ML str in
a_faire := !a_faire ^ byte;
a_faire_opt := !a_faire_opt ^ opt
@@ -325,25 +337,32 @@ let canonize f =
| (f,_) :: _ -> escape f
| _ -> escape f
+module VData = struct
+ type t = string list option * string list
+ let compare = Pervasives.compare
+end
+
+module VCache = Set.Make(VData)
+
let rec traite_fichier_Coq suffixe verbose f =
try
let chan = open_in f in
let buf = Lexing.from_channel chan in
- let deja_vu_v = ref ([]: (string list option * string list) list)
- and deja_vu_ml = ref ([] : string list) in
+ let deja_vu_v = ref VCache.empty in
+ let deja_vu_ml = ref StrSet.empty in
try
while true do
let tok = coq_action buf in
match tok with
| Require (from, strl) ->
List.iter (fun str ->
- if not (List.mem (from, str) !deja_vu_v) then begin
- addQueue deja_vu_v (from, str);
+ if not (VCache.mem (from, str) !deja_vu_v) then begin
+ deja_vu_v := VCache.add (from, str) !deja_vu_v;
try
let file_str = safe_assoc from verbose f str in
printf " %s%s" (canonize file_str) suffixe
with Not_found ->
- if verbose && not (Hashtbl.mem coqlibKnown str) then
+ if verbose && not (is_in_coqlib ?from str) then
warning_module_notfound f str
end) strl
| Declare sl ->
@@ -354,8 +373,8 @@ let rec traite_fichier_Coq suffixe verbose f =
in
let decl str =
let s = basename_noext str in
- if not (List.mem s !deja_vu_ml) then begin
- addQueue deja_vu_ml s;
+ if not (StrSet.mem s !deja_vu_ml) then begin
+ deja_vu_ml := StrSet.add s !deja_vu_ml;
match search_mllib_known s with
| Some mldir -> declare ".cma" mldir s
| None ->
@@ -369,8 +388,8 @@ let rec traite_fichier_Coq suffixe verbose f =
in List.iter decl sl
| Load str ->
let str = Filename.basename str in
- if not (List.mem (None, [str]) !deja_vu_v) then begin
- addQueue deja_vu_v (None, [str]);
+ if not (VCache.mem (None, [str]) !deja_vu_v) then begin
+ deja_vu_v := VCache.add (None, [str]) !deja_vu_v;
try
let (file_str, _) = Hashtbl.find vKnown [str] in
let canon = canonize file_str in
@@ -456,6 +475,14 @@ let add_caml_known phys_dir _ f =
| ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
| _ -> ()
+let add_coqlib_known recur phys_dir log_dir f =
+ match get_extension f [".vo"] with
+ | (basename,".vo") ->
+ let name = log_dir@[basename] in
+ let paths = if recur then suffixes name else [name] in
+ List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
+ | _ -> ()
+
let add_known recur phys_dir log_dir f =
match get_extension f [".v";".vo"] with
| (basename,".v") ->
@@ -475,7 +502,7 @@ let add_known recur phys_dir log_dir f =
(* Visits all the directories under [dir], including [dir] *)
let is_not_seen_directory phys_f =
- not (List.mem phys_f !norec_dirs)
+ not (StrSet.mem phys_f !norec_dirs)
let rec add_directory add_file phys_dir log_dir =
let f = function
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index dcd69ebdb..c3570f811 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -6,12 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+module StrSet : Set.S with type elt = string
+
val option_c : bool ref
val option_noglob : bool ref
val option_boot : bool ref
val option_natdynlk : bool ref
val option_mldep : string option ref
-val norec_dirs : string list ref
+val norec_dirs : StrSet.t ref
val suffixe : string ref
type dir = string option
val get_extension : string -> string list -> string * string
@@ -30,7 +32,6 @@ val search_mli_known : string -> dir option
val add_mllib_known : string -> dir -> string -> unit
val search_mllib_known : string -> dir option
val search_v_known : ?from:string list -> string list -> string option
-val coqlibKnown : (string list, unit) Hashtbl.t
val file_name : string -> string option -> string
val escape : string -> string
val canonize : string -> string
@@ -38,6 +39,7 @@ val mL_dependencies : unit -> unit
val coq_dependencies : unit -> unit
val suffixes : 'a list -> 'a list list
val add_known : bool -> string -> string list -> string -> unit
+val add_coqlib_known : bool -> string -> string list -> string -> unit
val add_caml_known : string -> string list -> string -> unit
val add_caml_dir : string -> unit
val add_dir :
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 19:10:52 +0000