Commit bf12eb93f3f6a6a824a10878878fadd59745aae0 - coq

+0

-8

~~.dir-locals.el~~ less more

0		((nil . ((eval . (setq default-directory (locate-dominating-file
1		buffer-file-name
2		".dir-locals.el")
3		tags-file-name (concat default-directory
4		"TAGS")
5		camldebug-command-name (concat
6		default-directory "dev/ocamldebug-coq")
7		)))))⏎

+0

-185

~~.gitignore~~ less more

0		*.glob
1		*.d
2		*.d.raw
3		*.vo
4		.cm
5		*.annot
6		*.spit
7		*.spot
8		*.o
9		*.a
10		*.log
11		*.aux
12		*.dvi
13		*.blg
14		*.bbl
15		*.idx
16		*.ilg
17		*.toc
18		*.atoc
19		*.comidx
20		*.comind
21		*.erridx
22		*.errind
23		*.haux
24		*.hcomind
25		*.herrind
26		*.hind
27		*.htacind
28		*.htoc
29		*.ind
30		*.lof
31		*.tacidx
32		*.tacind
33		*.v.tex
34		*.v.pdf
35		*.v.ps
36		*.v.html
37		*.stamp
38		revision
39		TAGS
40		.DS_Store
41		.pc
42		bin/
43		_build
44		plugins//_mod.ml
45		myocamlbuild_config.ml
46		config/Makefile
47		config/coq_config.ml
48		dev/ocamldebug-coq
49		plugins/micromega/csdpcert
50		kernel/byterun/dllcoqrun.so
51		states/initial.coq
52		coqdoc.sty
53		test-suite/lia.cache
54		test-suite/trace
55		test-suite/misc/universes/all_stdlib.v
56		test-suite/misc/universes/universes.txt
57
58		# documentation
59
60		doc/faq/html/
61		doc/refman/csdp.cache
62		doc/refman/trace
63		doc/refman/Reference-Manual.pdf
64		doc/refman/Reference-Manual.ps
65		doc/refman/Reference-Manual.html
66		doc/refman/Reference-Manual.out
67		doc/refman/Reference-Manual.sh
68		doc/refman/cover.html
69		doc/refman/styles.hva
70		doc/common/version.tex
71		doc/refman/coqide-queries.eps
72		doc/refman/coqide.eps
73		doc/refman/euclid.ml
74		doc/refman/euclid.mli
75		doc/refman/heapsort.ml
76		doc/refman/heapsort.mli
77		doc/refman/html/
78		doc/stdlib/Library.out
79		doc/stdlib/Library.pdf
80		doc/stdlib/Library.ps
81		doc/stdlib/Library.coqdoc.tex
82		doc/stdlib/FullLibrary.pdf
83		doc/stdlib/FullLibrary.ps
84		doc/stdlib/FullLibrary.coqdoc.tex
85		doc/stdlib/html/
86		doc/stdlib/index-body.html
87		doc/stdlib/index-list.html
88		doc/RecTutorial/RecTutorial.html
89		doc/RecTutorial/RecTutorial.pdf
90		doc/RecTutorial/RecTutorial.ps
91		dev/doc/naming-conventions.pdf
92
93		# .mll files
94
95		dev/ocamlweb-doc/lex.ml
96		ide/coq_lex.ml
97		ide/config_lexer.ml
98		ide/utf8_convert.ml
99		ide/highlight.ml
100		plugins/dp/dp_zenon.ml
101		tools/gallina_lexer.ml
102		tools/coqwc.ml
103		tools/coqdep_lexer.ml
104		tools/coqdoc/cpretty.ml
105		lib/xml_lexer.ml
106
107		# .mly files
108
109		ide/config_parser.ml
110		ide/config_parser.mli
111
112		# .ml4 files
113
114		ide/project_file.ml
115		lib/pp.ml
116		lib/compat.ml
117		parsing/g_xml.ml
118		parsing/g_prim.ml
119		parsing/q_util.ml
120		parsing/tacextend.ml
121		parsing/q_constr.ml
122		parsing/g_vernac.ml
123		parsing/pcoq.ml
124		parsing/g_constr.ml
125		parsing/g_ltac.ml
126		parsing/vernacextend.ml
127		parsing/g_tactic.ml
128		parsing/argextend.ml
129		parsing/g_decl_mode.ml
130		parsing/q_coqast.ml
131		parsing/g_proofs.ml
132		parsing/lexer.ml
133		plugins/xml/proofTree2Xml.ml
134		plugins/xml/acic2Xml.ml
135		plugins/xml/xml.ml
136		plugins/xml/dumptree.ml
137		plugins/xml/xmlentries.ml
138		plugins/extraction/g_extraction.ml
139		plugins/rtauto/g_rtauto.ml
140		plugins/romega/g_romega.ml
141		plugins/setoid_ring/newring.ml
142		plugins/firstorder/g_ground.ml
143		plugins/dp/g_dp.ml
144		plugins/cc/g_congruence.ml
145		plugins/ring/g_ring.ml
146		plugins/field/field.ml
147		plugins/funind/g_indfun.ml
148		plugins/omega/g_omega.ml
149		plugins/quote/g_quote.ml
150		plugins/nsatz/nsatz.ml
151		plugins/micromega/g_micromega.ml
152		plugins/subtac/g_subtac.ml
153		plugins/fourier/g_fourier.ml
154		plugins/decl_mode/g_decl_mode.ml
155		tactics/tauto.ml
156		tactics/eauto.ml
157		tactics/hipattern.ml
158		tactics/class_tactics.ml
159		tactics/rewrite.ml
160		tactics/eqdecide.ml
161		tactics/extratactics.ml
162		tactics/extraargs.ml
163		tools/coq_tex.ml
164		toplevel/mltop.ml
165		toplevel/whelp.ml
166		ide/coqide_main.ml
167		ide/coqide_main_opt.ml
168
169		# other auto-generated files
170
171		ide/undo.mli
172		toplevel/mltop.optml
173		toplevel/mltop.byteml
174		kernel/byterun/coq_jumptbl.h
175		kernel/copcodes.ml
176		scripts/tolink.ml
177		theories/Numbers/Natural/BigN/NMake_gen.v
178		ide/index_urls.txt
179
180		# mlis documentation
181
182		dev/ocamldoc/html/
183		dev/ocamldoc/coq.*
184		dev/ocamldoc/ocamldoc.sty

+32

-0

CHANGES less more

	0	Changes from V8.4 to V8.4pl1
	1	============================
	2
	3	Bug fixes
	4
	5	- Solved bugs :
	6	#2851 #2863 #2865 #2893 #2895 #2892 #2905 #2906 #2907 #2917 #2921
	7	#2930 #2941 #2878
	8	- Partially fixed bug : #2904
	9	- Various fixes concerning coq_makefile
	10
	11	Optimizations
	12
	13	- "Union by rank" optimization for universes contributed by J.H. Jourdan
	14	and G. Sherrer (see union-find-and-coq-universes on gagallium blog).
	15
	16	Libraries
	17
	18	- Internal organisation of some modular libraries have slightly changed
	19	due to bug #2904 (GenericMinMax, OrdersTac)
	20	- No more constant "int" in ZArith/Int.v to avoid name clash with OCaml
	21	(cf bug #2878).
	22
	23	Coqide
	24
	25	- Improved shutdown of coqtop processes spawned by coqide
	26	(in particular added a missing close_on_exec primitive before forking).
	27	- On windows, launching coqide with the -debug option now produces
	28	a log file in the user's temporary directory. The location of this
	29	log file is displayed in the "About" message.
	30
	31
0	32	Changes from V8.4beta2 to V8.4
1	33	==============================
2	34

+0

-4

INSTALL less more

153	153	-opt
154	154	Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt
155	155	compiler instead of ocamlopt). Makes compilation faster (recommended).
156
157		-nowarnings
158		Disable the Objective Caml compiler warnings. This option has no
159		effect on the result of the compilation.
160	156
161	157	-browser <command>
162	158	Use <command> to open an URL in a browser. %s must appear in <command>,

+29

-18

Makefile.build less more

83	83
84	84	LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
85	85	MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
86		COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB)
87	86
88	87	OCAMLC += $(CAMLFLAGS)
89	88	OCAMLOPT += $(CAMLFLAGS)
90	89
91		BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
92		OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
93		COREBYTEFLAGS=$(COREMLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
94		COREOPTFLAGS=$(COREMLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
	90	BAREBYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
	91	BAREOPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
	92	BYTEFLAGS=$(MLINCLUDES) $(BAREBYTEFLAGS)
	93	OPTFLAGS=$(MLINCLUDES) $(BAREOPTFLAGS)
95	94	DEPFLAGS= -slash $(LOCALINCLUDES)
96	95
97	96	define bestocaml

193	192	# Main targets (coqmktop, coqtop.opt, coqtop.byte)
194	193	###########################################################################
195	194
	195	## In Win32, cygwin provides an emulation of ln -s, but this emulation
	196	## won't work outside of cygwin shell (i.e. typically in a Sys.command).
	197	## So we just forget about it, and do a simple copy.
	198
	199	ifeq ($(ARCH),win32)
	200	LN:=cp -f
	201	else
	202	LN:=ln -sf
	203	endif
	204
196	205	.PHONY: coqbinaries coq coqlib coqlight states
197	206
198	207	coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}

207	216
208	217	$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN)
209	218	$(SHOW)'COQMKTOP -o $@'
210		$(HIDE)$(BESTCOQMKTOP) -boot -opt $(COREOPTFLAGS) -o $@
	219	$(HIDE)$(BESTCOQMKTOP) -boot -opt $(BAREOPTFLAGS) -o $@
211	220	$(STRIP) $@
212	221
213	222	$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN)
214	223	$(SHOW)'COQMKTOP -o $@'
215		$(HIDE)$(BESTCOQMKTOP) -boot -top $(COREBYTEFLAGS) -o $@
	224	$(HIDE)$(BESTCOQMKTOP) -boot -top $(BAREBYTEFLAGS) -o $@
216	225
217	226	$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
218		cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
	227	cd bin && $(LN) coqtop.$(BEST)$(EXE) coqtop$(EXE)
219	228
220	229	LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) )
221	230	CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB)

232	241	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^
233	242
234	243	$(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
235		cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
	244	cd bin && $(LN) coqchk.$(BEST)$(EXE) coqchk$(EXE)
236	245
237	246	# coqmktop
238	247

246	255	$(STRIP) $@
247	256
248	257	$(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP)
249		cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE)
	258	cd bin && $(LN) coqmktop.$(BEST)$(EXE) coqmktop$(EXE)
250	259
251	260	scripts/tolink.ml: Makefile.build Makefile.common
252	261	$(SHOW)"ECHO... >" $@

266	275	$(STRIP) $@
267	276
268	277	$(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC)
269		cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE)
	278	cd bin && $(LN) coqc.$(BEST)$(EXE) coqc$(EXE)
270	279
271	280	# target for libraries
272	281

319	328
320	329	$(COQIDEOPT): $(LINKIDEOPT) \| $(COQTOPOPT)
321	330	$(SHOW)'OCAMLOPT -o $@'
322		$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa\
323		gtkThread.cmx str.cmxa $(LINKIDEOPT)
	331	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa \
	332	lablgtk.cmxa $(IDEOPTFLAGS) gtkThread.cmx str.cmxa $(LINKIDEOPT)
324	333	$(STRIP) $@
325	334
326	335	$(COQIDEBYTE): $(LINKIDE) \| $(COQTOPBYTE)

329	338	str.cma $(COQRUNBYTEFLAGS) $(LINKIDE)
330	339
331	340	$(COQIDE):
332		cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
	341	cd bin && $(LN) coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
333	342
334	343	# install targets
335	344

345	354	$(INSTALLBIN) $(COQIDEBYTE) $(FULLBINDIR)
346	355	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
347	356	$(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
348		cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE)
	357	cd $(FULLBINDIR) && $(LN) coqide.byte$(EXE) coqide$(EXE)
349	358
350	359	install-ide-opt:
351	360	$(MKDIR) $(FULLBINDIR)
352	361	$(INSTALLBIN) $(COQIDEOPT) $(FULLBINDIR)
353	362	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) \
354	363	$(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
355		cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE)
	364	cd $(FULLBINDIR) && $(LN) coqide.opt$(EXE) coqide$(EXE)
356	365
357	366	install-ide-files:
358	367	$(MKDIR) $(FULLDATADIR)

603	612	install-byte::
604	613	$(MKDIR) $(FULLBINDIR)
605	614	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR)
606		cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE)
	615	cd $(FULLBINDIR); $(LN) coqtop.byte$(EXE) coqtop$(EXE); $(LN) coqchk.byte$(EXE) coqchk$(EXE)
607	616
608	617	install-opt::
609	618	$(MKDIR) $(FULLBINDIR)
610	619	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(FULLBINDIR)
611		cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE); ln -sf coqchk.opt$(EXE) coqchk$(EXE)
	620	cd $(FULLBINDIR); $(LN) coqtop.opt$(EXE) coqtop$(EXE); $(LN) coqchk.opt$(EXE) coqchk$(EXE)
612	621
613	622	install-tools::
614	623	$(MKDIR) $(FULLBINDIR)

632	641	$(MKDIR) $(FULLCOQLIB)/states
633	642	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
634	643	$(MKDIR) $(FULLCOQLIB)/user-contrib
	644	ifneq ($(COQRUNBYTEFLAGS),"-custom")
635	645	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
	646	endif
636	647	$(INSTALLSH) $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA)
637	648	$(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI)
638	649	ifeq ($(BEST),opt)

+2

-2

Makefile.common less more

118	118	HEVEAOPTS:=-fix -exec xxdate.exe
119	119	HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
120	120	HTMLSTYLE:=simple
121		export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB):
122		COQTEXOPTS:=-n 72 -image "$(COQSRC)/$(COQTOPEXE) -boot" -sl -small
	121	export TEXINPUTS:=$(HEVEALIB):
	122	COQTEXOPTS:=-boot -n 72 -sl -small
123	123
124	124	DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
125	125

+2

-2

Makefile.doc less more

52	52
53	53	ifdef QUICK
54	54	%.v.tex: %.tex
55		(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
	55	$(COQTEX) $(COQTEXOPTS) $<
56	56	else
57	57	%.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO)
58		(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
	58	$(COQTEX) $(COQTEXOPTS) $<
59	59	endif
60	60
61	61	%.ps: %.dvi

+0

-53

~~TODO~~ less more

0		Langage:
1
2		Distribution:
3
4		Environnement:
5
6		- Porter SearchIsos
7
8		Noyau:
9
10		Tactic:
11
12		- Que contradiction raisonne a isomorphisme pres de False
13
14		Vernac:
15
16		- Print / Print Proof en fait identiques ; Print ne devrait pas afficher
17		les constantes opaques (devrait afficher qqchose comme <opaque>)
18
19		Theories:
20
21		- Rendre transparent tous les theoremes prouvant {A}+{B}
22		- Faire demarrer PolyList.nth a` l'indice 0
23		Renommer l'actuel nth en nth1 ??
24
25		Doc:
26
27		- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
28		- Documenter le filtrage sur les types inductifs avec let-ins (dont la
29		compatibilite V6)
30
31		- Ajouter let dans les règles du CIC
32		-> FAIT, mais reste a documenter le let dans les inductifs
33		et les champs manifestes dans les Record
34		- revoir le chapitre sur les tactiques utilisateur
35		- faut-il mieux spécifier la sémantique de Simpl (??)
36
37		- Préciser la clarification syntaxique de IntroPattern
38		- preciser que Goal vient en dernier dans une clause pattern list et
39		qu'il doit apparaitre si il y a un "in"
40
41		- Omega Time debranche mais Omega System et Omega Action remarchent ?
42		- Ajout "Replace in" (mais TODO)
43		- Syntaxe Conditional tac Rewrite marche, à documenter
44		- Documenter Dependent Rewrite et CutRewrite ?
45		- Ajouter les motifs sous-termes de ltac
46
47		- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.)
48		- mettre à jour la doc de induction (arguments multiples) (Pierre C.)
49		- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.)
50		--> mettre à jour le CHANGES (vers la ligne 72)
51
52

+4

-2

build less more

11	11	[ -L $MYCFG ] \|\| ln -sf $CFG $MYCFG
12	12	}
13	13
14		ocb() { $OCAMLBUILD $FLAGS $*; }
	14	# NB: we exec ocamlbuild and run ocb last for a correct exit code
	15
	16	ocb() { exec $OCAMLBUILD $FLAGS $*; }
15	17
16	18	rule() {
17	19	check_config
18	20	case $1 in
19		clean) ocb -clean && rm -rf bin/* && rm -f $MYCFG;;
	21	clean) rm -rf bin/* $MYCFG && ocb -clean;;
20	22	all) ocb coq.otarget;;
21	23	win32) ocb coq-win32.otarget;;
22	24	*) ocb $1;;

+52

-44

configure less more

5	5	#
6	6	##################################
7	7
8		VERSION=8.4
	8	VERSION=8.4pl1
9	9	VOMAGIC=08400
10	10	STATEMAGIC=58400
11	11	DATE=`LC_ALL=C LANG=C date +"%B %Y"`

34	34	printf "\tSet installation directory to <dir>\n"
35	35	echo "-local"
36	36	printf "\tSet installation directory to the current source tree\n"
37		echo "-coqrunbyteflags"
	37	echo "-coqrunbyteflags <flags>"
38	38	printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
39		echo "-coqtoolsbyteflags"
	39	echo "-coqtoolsbyteflags <flags>"
40	40	printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
41	41	echo "-custom"
42	42	printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
43		echo "-src"
	43	echo "-src <dir>"
44	44	printf "\tSpecifies the source directory\n"
45		echo "-bindir"
46		echo "-libdir"
47		echo "-configdir"
48		echo "-datadir"
49		echo "-mandir"
50		echo "-docdir"
	45	echo "-bindir <dir>"
	46	echo "-libdir <dir>"
	47	echo "-configdir <dir>"
	48	echo "-datadir <dir>"
	49	echo "-mandir <dir>"
	50	echo "-docdir <dir>"
51	51	printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n"
52		echo "-emacslib"
53		echo "-emacs"
	52	echo "-emacslib <dir>"
54	53	printf "\tSpecifies where emacs files are to be installed\n"
55		echo "-coqdocdir"
	54	echo "-coqdocdir <dir>"
56	55	printf "\tSpecifies where Coqdoc style files are to be installed\n"
57		echo "-camldir"
	56	echo "-camldir <dir>"
58	57	printf "\tSpecifies the path to the OCaml library\n"
59		echo "-lablgtkdir"
	58	echo "-lablgtkdir <dir>"
60	59	printf "\tSpecifies the path to the Lablgtk library\n"
61	60	echo "-usecamlp5"
62	61	printf "\tSpecifies to use camlp5 instead of camlp4\n"
63	62	echo "-usecamlp4"
64	63	printf "\tSpecifies to use camlp4 instead of camlp5\n"
65		echo "-camlp5dir"
	64	echo "-camlp5dir <dir>"
66	65	printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
67		echo "-arch"
	66	echo "-arch <arch>"
68	67	printf "\tSpecifies the architecture\n"
69	68	echo "-opt"
70	69	printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"

162	161	-coqtoolsbyteflags\|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
163	162	coqtoolsbyteflags="$2"
164	163	shift;;
165		-custom\|--custom) custom_spec=yes
166		shift;;
	164	-custom\|--custom) custom_spec=yes;;
167	165	-src\|--src) src_spec=yes
168	166	COQSRC="$2"
169	167	shift;;

190	188	shift;;
191	189	-emacs \|--emacs) emacs_spec=yes
192	190	emacs="$2"
	191	printf "Warning: obsolete -emacs option\n"
193	192	shift;;
194	193	-coqdocdir\|--coqdocdir) coqdocdir_spec=yes
195	194	coqdocdir="$2"

594	593	# OS dependent libraries
595	594
596	595	OSDEPLIBS="-cclib -lunix"
597		case $ARCH,$CYGWIN in
	596	case $ARCH in
598	597	sun4*) OS=`uname -r`
599	598	case $OS in
600	599	5*) OS="Sun Solaris $OS"
601	600	OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";;
602	601	*) OS="Sun OS $OS"
603	602	esac;;
604		win32,yes) OS="Win32 (Cygwin)"
605		cflags="-mno-cygwin $cflags";;
606		win32,*) OS="Win32 (MinGW)";;
607	603	esac
608	604
609	605	# lablgtk2 and CoqIDE

626	622	else
627	623	case $lablgtkdir_spec in
628	624	no)
629		if lablgtkdir=$(ocamlfind query lablgtk2 2> /dev/null); then
630		lablgtkdir_spec=yes
631		elif [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
	625	if lablgtkdirtmp=$(ocamlfind query lablgtk2 2> /dev/null); then
	626	if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then
	627	lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind"
	628	lablgtkdir=$lablgtkdirtmp
	629	LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
	630	else
	631	echo "Headers missings in Lablgtk2 found by ocamlfind (glib.cmi/glib.mli not found)."
	632	fi
	633	fi
	634	if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.mli" -a -f "${CAMLLIB}/glib.mli" ]; then
	635	lablgtkdirfoundmsg="LablGtk2 found in ocaml lib directory"
632	636	lablgtkdir=${CAMLLIB}/lablgtk2
	637	LABLGTKLIB=+lablgtk2 # Pour le message utilisateur
633	638	fi;;
634	639	yes)
635		if [ ! -f "$lablgtkdir/glib.mli" ]; then
636		echo "Incorrect LablGtk2 library (glib.mli not found)."
	640	if [ ! -d "$lablgtkdir" ]; then
	641	echo "$lablgtkdir is not a valid directory."
	642	echo "Configuration script failed!"
	643	exit 1
	644	elif [ -f "$lablgtkdir/glib.cmi" -a -f "$lablgtkdir/glib.mli" ]; then
	645	lablgtkdirfoundmsg="LablGtk2 directory found"
	646	LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
	647	else
	648	echo "Headers missing in LablGtk2 library (glib.cmi/glib.mli not found)."
637	649	echo "Configuration script failed!"
638	650	exit 1
639	651	fi;;

642	654	echo "LablGtk2 not found: CoqIde will not be available."
643	655	COQIDE=no
644	656	elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
645		echo "LablGtk2 found but too old: CoqIde will not be available."
	657	echo "$lablgtkdirfoundmsg but too old: CoqIde will not be available."
646	658	COQIDE=no;
647	659	elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then
648		echo "LablGtk2 found, bytecode CoqIde will be used as requested."
	660	echo "$lablgtkdirfoundmsg, bytecode CoqIde will be used as requested."
649	661	COQIDE=byte
650	662	elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then
651		echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
	663	echo "$lablgtkdirfoundmsg, no native threads: bytecode CoqIde will be available."
652	664	COQIDE=byte
653	665	else
654		echo "LablGtk2 found, native threads: native CoqIde will be available."
	666	echo "$lablgtkdirfoundmsg, native threads: native CoqIde will be available."
655	667	COQIDE=opt
656		if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration;
	668	if [ "$nomacintegration_spec" = "no" ] && lablgtkosxdir=$(ocamlfind query lablgtkosx 2> /dev/null);
657	669	then
658		cflags=$cflags" `pkg-config --cflags gtk-mac-integration`"
659		IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"'
660		IDEARCHFILE=ide/ide_mac_stubs.o
	670	IDEARCHFLAGS=lablgtkosx.cmxa
661	671	IDEARCHDEF=QUARTZ
662	672	elif [ "$ARCH" = "win32" ];
663	673	then

670	680
671	681	case $COQIDE in
672	682	byte\|opt)
673		case $lablgtkdir_spec in
674		no) LABLGTKLIB=+lablgtk2 # Pour le message
675		LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
676		yes) LABLGTKLIB=$lablgtkdir # Pour le message
677		LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
678		esac;;
679		no) LABLGTKINCLUDES="";;
680		esac
	683	LABLGTKINCLUDES="-I $LABLGTKLIB";;
	684	no)
	685	LABLGTKINCLUDES="";;
	686	esac
	687
	688	[ x$lablgtkosxdir = x ] \|\| LABLGTKINCLUDES="$LABLGTKINCLUDES -I $lablgtkosxdir"
681	689
682	690	# strip command
683	691

+27

-38

doc/common/styles/html/coqremote/footer.html less more

0		<div id="sidebarWrapper">
1		<div id="sidebar">
	0	<div id="sidebarWrapper">
	1	<div id="sidebar">
	2	<div class="block">
	3	<h2 class="title">Navigation</h2>
	4	<div class="content">
	5	<ul class="menu">
	6	<li class="leaf">Standard Library
	7	<ul class="menu">
	8	<li><a href="index.html">Table of contents</a></li>
	9	<li><a href="genindex.html">Index</a></li>
	10	</ul>
	11	</li>
	12	</ul>
	13	</div>
	14	</div>
	15	</div>
	16	</div>
2	17
3		<div class="block">
4		<h2 class="title">Navigation</h2>
5		<div class="content">
	18	</div>
6	19
7		<ul class="menu">
8
9		<li class="leaf">Standard Library
10		<ul class="menu">
11		<li><a href="index.html">Table of contents</a></li>
12		<li><a href="genindex.html">Index</a></li>
13		</ul>
14		</li>
15
16		</ul>
17
18		</div>
19		</div>
20
21		</div>
22		</div>
23
24
25		</div>
26
27		</div>
28
29		<div id="footer">
30		<div id="nav-footer">
31		<ul class="links-menu-footer">
32		<li><a href="mailto:webmaster_@_www.lix.polytechnique.fr">webmaster</a></li>
33		<li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li>
34		<li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li>
35		</ul>
36
37		</div>
38		</div>
	20	<div id="footer">
	21	<div id="nav-footer">
	22	<ul class="links-menu-footer">
	23	<li><a href="mailto:www-coq_@_lix.polytechnique.fr">webmaster</a></li>
	24	<li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li>
	25	<li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li>
	26	</ul>
	27	</div>
	28	</div>
39	29
40	30	</div>
41	31
42	32	</body>
43	33	</html>
44

+26

-30

doc/common/styles/html/coqremote/header.html less more

5	5	<title>Standard Library \| The Coq Proof Assistant</title>
6	6
7	7	<link rel="shortcut icon" href="favicon.ico" type="image/x-icon" />
8		<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/node/node.css";</style>
	8	<style type="text/css" media="all">@import "http://coq.inria.fr/modules/node/node.css";</style>
9	9
10		<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/system/defaults.css";</style>
11		<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/system/system.css";</style>
12		<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/modules/user/user.css";</style>
	10	<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/defaults.css";</style>
	11	<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/system.css";</style>
	12	<style type="text/css" media="all">@import "http://coq.inria.fr/modules/user/user.css";</style>
13	13
14		<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/sites/all/themes/coq/style.css";</style>
15		<style type="text/css" media="all">@import "http://www.lix.polytechnique.fr/coq/sites/all/themes/coq/coqdoc.css";</style>
	14	<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</style>
	15	<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</style>
16	16
17	17	</head>
18	18
19	19	<body>
20	20
21	21	<div id="container">
22		<div id="headertop">
23		<div id="nav">
24		<ul class="links-menu">
25		<li><a href="http://www.lix.polytechnique.fr/coq/" class="active">Home</a></li>
	22	<div id="headertop">
	23	<div id="nav">
	24	<ul class="links-menu">
	25	<li><a href="http://coq.inria.fr/" class="active">Home</a></li>
	26	<li><a href="http://coq.inria.fr/about-coq" title="More about coq">About Coq</a></li>
	27	<li><a href="http://coq.inria.fr/download">Get Coq</a></li>
	28	<li><a href="http://coq.inria.fr/documentation">Documentation</a></li>
	29	<li><a href="http://coq.inria.fr/community">Community</a></li>
	30	</ul>
	31	</div>
	32	</div>
26	33
27		<li><a href="http://www.lix.polytechnique.fr/coq/about-coq" title="More about coq">About Coq</a></li>
28		<li><a href="http://www.lix.polytechnique.fr/coq/download">Get Coq</a></li>
29		<li><a href="http://www.lix.polytechnique.fr/coq/documentation">Documentation</a></li>
30		<li><a href="http://www.lix.polytechnique.fr/coq/community">Community</a></li>
31		</ul>
32		</div>
33		</div>
	34	<div id="header">
	35	<div id="logoWrapper">
	36	<div id="logo"><a href="http://coq.inria.fr/" title="Home"><img src="http://coq.inria.fr/files/barron_logo.png" alt="Home" /></a>
	37	</div>
	38	<div id="siteName"><a href="http://coq.inria.fr/" title="Home">The Coq Proof Assistant</a>
	39	</div>
	40	</div>
	41	</div>
34	42
35		<div id="header">
	43	<div id="content">
36	44
37		<div id="logoWrapper">
38
39		<div id="logo"><a href="http://www.lix.polytechnique.fr/coq/" title="Home"><img src="http://www.lix.polytechnique.fr/coq/files/barron_logo.png" alt="Home" /></a>
40		</div>
41		<div id="siteName"><a href="http://www.lix.polytechnique.fr/coq/" title="Home">The Coq Proof Assistant</a>
42		</div>
43
44		</div>
45		</div>
46
47		<div id="content">
48

+19

-1

ide/coq.ml less more

190	190
191	191	Note: we use Unix.stderr in Unix.create_process to get debug
192	192	messages from the coqtop's Ide_slave loop.
	193
	194	NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r)
	195	in coqtop. We do this indirectly via [Unix.set_close_on_exec].
	196	This way, coqide has the only remaining copies of these descriptors,
	197	and closing them later will have visible effects in coqtop. Cf man 7 pipe :
	198
	199	- If all file descriptors referring to the write end of a pipe have been
	200	closed, then an attempt to read(2) from the pipe will see end-of-file
	201	(read(2) will return 0).
	202	- If all file descriptors referring to the read end of a pipe have been
	203	closed, then a write(2) will cause a SIGPIPE signal to be generated for
	204	the calling process. If the calling process is ignoring this signal,
	205	then write(2) fails with the error EPIPE.
	206
	207	Symmetrically, coqtop's descriptors (ide2top_r and top2ide_w) should be
	208	closed in coqide.
193	209	*)
194	210
195	211	let open_process_pid prog args =
196	212	let (ide2top_r,ide2top_w) = Unix.pipe () in
197	213	let (top2ide_r,top2ide_w) = Unix.pipe () in
	214	Unix.set_close_on_exec ide2top_w;
	215	Unix.set_close_on_exec top2ide_r;
198	216	let pid = Unix.create_process prog args ide2top_r top2ide_w Unix.stderr in
199	217	assert (pid <> 0);
200	218	Unix.close ide2top_r;

249	267	Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c);
250	268	flush coqtop.cin;
251	269	let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
252		(Ide_intf.to_answer xml : 'a Interface.value)
	270	(Ide_intf.to_answer xml c : 'a Interface.value)
253	271
254	272	let interp coqtop ?(raw=false) ?(verbose=true) s =
255	273	eval_call coqtop (Ide_intf.interp (raw,verbose,s))

+81

-102

ide/coqide.ml less more

40	40	val mutable read_only : bool
41	41	val mutable filename : string option
42	42	val mutable stats : Unix.stats option
43		val mutable detached_views : GWindow.window list
44	43	method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b
45	44	method set_auto_complete : bool -> unit
46
47		method kill_detached_views : unit -> unit
48		method add_detached_view : GWindow.window -> unit
49		method remove_detached_view : GWindow.window -> unit
50	45
51	46	method filename : string option
52	47	method stats : Unix.stats option

103	98	}
104	99
105	100	let kill_session s =
106		s.analyzed_view#kill_detached_views ();
	101	(* To close the detached views of this script, we call manually
	102	[destroy] on it, triggering some callbacks in [detach_view].
	103	In a more modern lablgtk, rather use the page-removed signal ? *)
	104	s.script#destroy ();
107	105	Coq.kill_coqtop !(s.toplvl)
108	106
109	107	let build_session s =

441	439	Tags.Script.proof_decl; Tags.Script.qed ]
442	440
443	441	(** Cut a part of the buffer in sentences and tag them.
	442	Invariant: either this slice ends the buffer, or it ends with ".".
444	443	May raise [Coq_lex.Unterminated] when the zone ends with
445	444	an unterminated sentence. *)
446	445

479	478
480	479	(** Search backward the first character of a sentence, starting at [iter]
481	480	and going at most up to [soi] (meant to be the end of the locked zone).
482		Raise [Not_found] when no proper sentence start has been found,
483		in particular when the final "." of the locked zone is followed
484		by a non-blank character outside the locked zone. This non-blank
485		character will be signaled as erroneous in [tag_on_insert] below. *)
	481	Raise [StartError] when no proper sentence start has been found.
	482	A character following a ending "." is considered as a sentence start
	483	only if this character is a blank. In particular, when a final "."
	484	at the end of the locked zone isn't followed by a blank, then this
	485	non-blank character will be signaled as erroneous in [tag_on_insert] below.
	486	*)
	487
	488	exception StartError
486	489
487	490	let grab_sentence_start (iter:GText.iter) soi =
488	491	let cond iter =
489		if iter#compare soi < 0 then raise Not_found;
	492	if iter#compare soi < 0 then raise StartError;
490	493	let prev = iter#backward_char in
491	494	is_sentence_end prev &&
492	495	(not (is_char prev '.') \|\|

508	511
509	512	(** Retag a zone that has been edited *)
510	513
511		let tag_on_insert =
512		(* possible race condition here : editing two buffers with a timedelta smaller
513		* than 1.5s might break the error recovery mechanism. *)
514		let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *)
515		fun buffer ->
516		try
517		(* the start of the non-locked zone *)
518		let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
519		(* the inserted zone is between [prev_insert] and [insert] *)
520		let insert = buffer#get_iter_at_mark `INSERT in
521		let prev_insert = buffer#get_iter_at_mark (`NAME "prev_insert") in
522		(* [prev_insert] is normally always before [insert] even when deleting.
523		Let's check this nonetheless *)
524		let prev_insert =
525		if insert#compare prev_insert < 0 then insert else prev_insert
526		in
527		let start = grab_sentence_start prev_insert soi in
528		(** The status of "{" "}" as sentence delimiters is too fragile.
529		We retag up to the next "." instead. *)
530		let stop = grab_ending_dot insert in
531		let skip_curr = ref true in (* shall the callback be skipped ? by default yes*)
532		(!skip_last) := true; (* skip the previously created callback *)
533		skip_last := skip_curr;
534		try split_slice_lax buffer start stop
535		with Coq_lex.Unterminated ->
536		skip_curr := false;
537		let callback () =
538		if not !skip_curr then begin
539		try split_slice_lax buffer start buffer#end_iter
540		with Coq_lex.Unterminated -> ()
541		end; false
542		in
543		ignore (Glib.Timeout.add ~ms:1500 ~callback)
544		with Not_found ->
545		let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in
546		buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char
	514	let tag_on_insert buffer =
	515	(* the start of the non-locked zone *)
	516	let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
	517	(* the inserted zone is between [prev_insert] and [insert] *)
	518	let insert = buffer#get_iter_at_mark `INSERT in
	519	let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
	520	(* [prev] is normally always before [insert] even when deleting.
	521	Let's check this nonetheless *)
	522	let prev, insert =
	523	if insert#compare prev < 0 then insert, prev else prev, insert
	524	in
	525	try
	526	let start = grab_sentence_start prev soi in
	527	(** The status of "{" "}" as sentence delimiters is too fragile.
	528	We retag up to the next "." instead. *)
	529	let stop = grab_ending_dot insert in
	530	try split_slice_lax buffer start stop
	531	with Coq_lex.Unterminated ->
	532	(* This shouldn't happen frequently. Either:
	533	- we are at eof, with indeed an unfinished sentence.
	534	- we have just inserted an opening of comment or string.
	535	- the inserted text ends with a "." that interacts with the "."
	536	found by [grab_ending_dot] to form a non-ending "..".
	537	In any case, we retag up to eof, since this isn't that costly. *)
	538	if not stop#is_end then
	539	try split_slice_lax buffer start buffer#end_iter
	540	with Coq_lex.Unterminated -> ()
	541	with StartError ->
	542	buffer#apply_tag Tags.Script.error ~start:soi ~stop:soi#forward_char
547	543
548	544	let force_retag buffer =
549	545	try split_slice_lax buffer buffer#start_iter buffer#end_iter

590	586	val mutable stats = None
591	587	val mutable last_modification_time = 0.
592	588	val mutable last_auto_save_time = 0.
593		val mutable detached_views = []
594	589	val mutable find_forward_instead_of_backward = false
595	590
596	591	val mutable auto_complete_on = !current.auto_complete

605	600	let y = f x in
606	601	self#set_auto_complete old;
607	602	y
608		method add_detached_view (w:GWindow.window) =
609		detached_views <- w::detached_views
610		method remove_detached_view (w:GWindow.window) =
611		detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views
612
613		method kill_detached_views () =
614		List.iter (fun w -> w#destroy ()) detached_views;
615		detached_views <- []
616	603
617	604	method filename = filename
618	605	method stats = stats

819	806	begin
820	807	let menu_callback = if !current.contextual_menus_on_goal then
821	808	(fun s () -> ignore (self#insert_this_phrase_on_success
822		true true false ("progress "^s) s))
	809	true true false ("progress "^s) s))
823	810	else
824	811	(fun _ _ -> ()) in
825	812	try

1006	993	if stop#starts_line then
1007	994	input_buffer#insert ~iter:stop insertphrase
1008	995	else input_buffer#insert ~iter:stop ("\n"^insertphrase);
	996	tag_on_insert input_buffer;
1009	997	let start = self#get_start_of_input in
1010	998	input_buffer#move_mark ~where:stop (`NAME "start_of_input");
1011	999	input_buffer#apply_tag (safety_tag safe) ~start ~stop;

1230	1218	(List.exists
1231	1219	(fun p ->
1232	1220	self#insert_this_phrase_on_success true false false
1233		("progress "^p^".\n") (p^".\n")) l)
	1221	("progress "^p^".") (p^".")) l)
1234	1222
1235	1223	method active_keypress_handler k =
1236	1224	let state = GdkEvent.Key.state k in

1381	1369	);
1382	1370	ignore (input_buffer#connect#begin_user_action
1383	1371	~callback:(fun () ->
1384		let here = input_buffer#get_iter_at_mark `INSERT in
1385		input_buffer#move_mark (`NAME "prev_insert") here
1386		)
	1372	let where = self#get_insert in
	1373	input_buffer#move_mark (`NAME "prev_insert") ~where;
	1374	let start = self#get_start_of_input in
	1375	let stop = input_buffer#end_iter in
	1376	input_buffer#remove_tag Tags.Script.error ~start ~stop)
1387	1377	);
1388	1378	ignore (input_buffer#connect#end_user_action
1389	1379	~callback:(fun () ->
1390	1380	last_modification_time <- Unix.time ();
1391		let r = input_view#visible_rect in
1392		let stop =
1393		input_view#get_iter_at_location
1394		~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
1395		~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
1396		in
1397		input_buffer#remove_tag
1398		Tags.Script.error
1399		~start:self#get_start_of_input
1400		~stop;
1401	1381	tag_on_insert input_buffer
1402	1382	)
1403	1383	);

1794	1774	end
1795	1775	else false)
1796	1776
	1777	let logfile = ref None
	1778
1797	1779	let main files =
1798	1780
1799	1781	(* Main window *)

2353	2335	let tactic_shortcut s sc = GAction.add_action s ~label:("_"^s)
2354	2336	~accel:(!current.modifier_for_tactics^sc)
2355	2337	~callback:(do_if_active (fun a -> a#insert_command
2356		("progress "^s^".\n") (s^".\n"))) in
	2338	("progress "^s^".") (s^"."))) in
2357	2339	let query_callback command _ =
2358	2340	let word = get_current_word () in
2359	2341	if not (word = "") then

2379	2361	match key with
2380	2362	\|Some ac -> GAction.add_action name ~label ~callback ~accel:(!current.modifier_for_templates^ac)
2381	2363	\|None -> GAction.add_action name ~label ~callback ?accel:None
	2364	in
	2365	let detach_view _ =
	2366	(* Open a separate window containing the current buffer *)
	2367	let trm = session_notebook#current_term in
	2368	let w = GWindow.window ~show:true
	2369	~width:(!current.window_width*2/3)
	2370	~height:(!current.window_height*2/3)
	2371	~position:`CENTER
	2372	~title:(if trm.filename = "" then "scratch" else trm.filename)
	2373	()
	2374	in
	2375	let sb = GBin.scrolled_window ~packing:w#add ()
	2376	in
	2377	let nv = GText.view ~buffer:trm.script#buffer ~packing:sb#add ()
	2378	in
	2379	nv#misc#modify_font !current.text_font;
	2380	(* If the buffer in the main window is closed, destroy this detached view *)
	2381	ignore (trm.script#connect#destroy ~callback:w#destroy)
2382	2382	in
2383	2383	GAction.add_actions file_actions [
2384	2384	GAction.add_action "File" ~label:"_File";

2567	2567	];
2568	2568	GAction.add_actions windows_actions [
2569	2569	GAction.add_action "Windows" ~label:"_Windows";
2570		GAction.add_action "Detach View" ~label:"Detach _View"
2571		~callback:(fun _ -> do_if_not_computing "detach view"
2572		(function {script=v;analyzed_view=av} ->
2573		let w = GWindow.window ~show:true
2574		~width:(!current.window_width*2/3)
2575		~height:(!current.window_height*2/3)
2576		~position:`CENTER
2577		~title:(match av#filename with
2578		\| None -> "Unnamed"
2579		\| Some f -> f)
2580		()
2581		in
2582		let sb = GBin.scrolled_window
2583		~packing:w#add ()
2584		in
2585		let nv = GText.view
2586		~buffer:v#buffer
2587		~packing:sb#add
2588		()
2589		in
2590		nv#misc#modify_font
2591		!current.text_font;
2592		ignore (w#connect#destroy
2593		~callback:
2594		(fun () -> av#remove_detached_view w));
2595		av#add_detached_view w)
2596		[session_notebook#current_term]);
	2570	GAction.add_action "Detach View" ~label:"Detach _View" ~callback:detach_view
2597	2571	];
2598	2572	GAction.add_actions help_actions [
2599	2573	GAction.add_action "Help" ~label:"_Help";

2845	2819	\n-------------------\
2846	2820	\n"
2847	2821	in
	2822	let display_log_file (b:GText.buffer) =
	2823	if !debug then
	2824	let file = match !logfile with None -> "stderr" \| Some f -> f in
	2825	b#insert ("Debug mode is on, log file is "^file)
	2826	in
2848	2827	let initial_about (b:GText.buffer) =
2849	2828	let initial_string =
2850	2829	"Welcome to CoqIDE, an Integrated Development Environment for Coq\n"
2851	2830	in
2852	2831	let coq_version = Coq.short_version () in
2853		b#insert ~iter:b#start_iter "\n\n";
	2832	display_log_file b;
2854	2833	if Glib.Utf8.validate ("You are running " ^ coq_version) then
2855	2834	b#insert ~iter:b#start_iter ("You are running " ^ coq_version);
2856	2835	if Glib.Utf8.validate initial_string then

2880	2859	then b#insert about_full_string;
2881	2860	let coq_version = Coq.version () in
2882	2861	if Glib.Utf8.validate coq_version
2883		then b#insert coq_version
2884
	2862	then b#insert coq_version;
	2863	display_log_file b;
2885	2864	in
2886	2865	(* Remove default pango menu for textviews *)
2887	2866	w#show ();

+3

-0

ide/coqide.mli less more

10	10	(** The arguments that will be passed to coqtop. No quoting here, since
11	11	no /bin/sh when using create_process instead of open_process. *)
12	12	val sup_args : string list ref
	13
	14	(** In debug mode under win32, messages are written to a log file *)
	15	val logfile : string option ref
13	16
14	17	(** Filter the argv from coqide specific options, and set
15	18	Minilib.coqtop_path accordingly *)

+58

-24

ide/coqide_main.ml4 less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		IFDEF QUARTZ THEN
9		external gtk_mac_init : (string -> unit) -> (unit -> bool) -> unit
10		= "caml_gtk_mac_init"
	8	let _ = Coqide.ignore_break ()
	9	let _ = GtkMain.Main.init ()
11	10
12		external gtk_mac_ready : ([> Gtk.widget ] as 'a) Gtk.obj -> ([> Gtk.widget ] as 'a) Gtk.obj ->
13		([> Gtk.widget ] as 'a) Gtk.obj -> unit
14		= "caml_gtk_mac_ready"
15		END
	11	(* We handle Gtk warning messages ourselves :
	12	- on win32, we don't want them to end on a non-existing console
	13	- we display critical messages via pop-ups *)
16	14
17		let initmac () = IFDEF QUARTZ THEN gtk_mac_init Coqide.do_load Coqide.forbid_quit_to_save ELSE () END
	15	let catch_gtk_messages () =
	16	let all_levels =
	17	[`FLAG_RECURSION;`FLAG_FATAL;`ERROR;`CRITICAL;`WARNING;
	18	`MESSAGE;`INFO;`DEBUG]
	19	in
	20	let handler ~level msg =
	21	let header = "Coqide internal error: " in
	22	let level_is tag = (level land Glib.Message.log_level tag) <> 0 in
	23	if level_is `ERROR then
	24	let () = GToolbox.message_box ~title:"Error" (header ^ msg) in
	25	Coqide.crash_save 1
	26	else if level_is `CRITICAL then
	27	GToolbox.message_box ~title:"Error" (header ^ msg)
	28	else if level_is `DEBUG \|\| Sys.os_type = "Win32" then
	29	Ideutils.prerr_endline msg (* no-op unless in debug mode *)
	30	else
	31	Printf.eprintf "%s\n" msg
	32	in
	33	let catch domain =
	34	ignore (Glib.Message.set_log_handler ~domain ~levels:all_levels handler)
	35	in
	36	List.iter catch ["GLib";"Gtk";"Gdk";"Pango"]
18	37
19		let macready x y z = IFDEF QUARTZ THEN gtk_mac_ready x#as_widget y#as_widget z#as_widget ELSE () END
	38	let () = catch_gtk_messages ()
20	39
21	40	(* On win32, we add the directory of coqide to the PATH at launch-time
22	41	(this used to be done in a .bat script). *)

32	51	*)
33	52
34	53	let reroute_stdout_stderr () =
	54	(* We anticipate a bit the argument parsing and look for -debug *)
	55	let debug = List.mem "-debug" (Array.to_list Sys.argv) in
	56	Ideutils.debug := debug;
35	57	let out_descr =
36		if !Ideutils.debug then
37		Unix.descr_of_out_channel (snd (Filename.open_temp_file "coqide_" ".log"))
	58	if debug then
	59	let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
	60	Coqide.logfile := Some name;
	61	Unix.descr_of_out_channel chan
38	62	else
39	63	snd (Unix.pipe ())
40	64	in
	65	Unix.set_close_on_exec out_descr;
41	66	Unix.dup2 out_descr Unix.stdout;
42	67	Unix.dup2 out_descr Unix.stderr
43	68

63	88	reroute_stdout_stderr ()
64	89	END
65	90
	91	IFDEF QUARTZ THEN
	92	let osx = GosxApplication.osxapplication ()
	93
	94	let _ =
	95	osx#connect#ns_application_open_file ~callback:(fun x -> Coqide.do_load x; true) in
	96	let _ =
	97	osx#connect#ns_application_block_termination ~callback:Coqide.forbid_quit_to_save in
	98	()
	99	END
	100
66	101	let () =
67		Coqide.ignore_break ();
68		ignore (GtkMain.Main.init ());
69		initmac () ;
70	102	(try
71	103	let gtkrcdir = List.find
72	104	(fun x -> Sys.file_exists (Filename.concat x "coqide-gtk2rc"))

81	113	end;
82	114	(* GtkData.AccelGroup.set_default_mod_mask
83	115	(Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);*)
84		ignore (
85		Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
86		`WARNING;`CRITICAL]
87		(fun ~level msg ->
88		if level land Glib.Message.log_level `WARNING <> 0
89		then Printf.eprintf "Warning: %s\n" msg
90		else failwith ("Coqide internal error: " ^ msg)));
91	116	let argl = Array.to_list Sys.argv in
92	117	let argl = Coqide.read_coqide_args argl in
93	118	let files = Coq.filter_coq_opts (List.tl argl) in

95	120	Coq.check_connection args;
96	121	Coqide.sup_args := args;
97	122	Coqide.main files;
98		if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ());
99		macready (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar") (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")
100		(Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help/Abt");
	123	if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ())
	124
	125	IFDEF QUARTZ THEN
	126	let () =
	127	GtkosxApplication.Application.set_menu_bar osx#as_osxapplication (GtkMenu.MenuShell.cast (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) in
	128	let () =
	129	GtkosxApplication.Application.insert_app_menu_item osx#as_osxapplication (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 in
	130	let () =
	131	GtkosxApplication.Application.set_help_menu osx#as_osxapplication (Some (GtkMenu.MenuItem.cast (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) in
	132	osx#ready ()
	133	END
	134
101	135	while true do
102	136	try
103	137	GtkThread.main ()

+0

-85

~~ide/ide_mac_stubs.c~~ less more

0		#include <caml/mlvalues.h>
1		#include <caml/alloc.h>
2		#include <caml/memory.h>
3		#include <caml/callback.h>
4		#include <caml/fail.h>
5
6		#include <gtk/gtk.h>
7		#include <lablgtk2/wrappers.h>
8		#include <lablgtk2/ml_glib.h>
9		#include <lablgtk2/ml_gobject.h>
10		#include <gtkmacintegration/gtkosxapplication.h>
11
12		GtkOSXApplication *theApp;
13		value open_file_fun, forbid_quit_fun, themenubar, pref_item, about_item;
14
15		static void osx_accel_map_foreach_lcb(gpointer data,const gchar *accel_path,
16		guint accel_key, GdkModifierType accel_mods,
17		gboolean changed) {
18		if (accel_mods & GDK_CONTROL_MASK) {
19		accel_mods \|= GDK_META_MASK;
20		accel_mods &= (accel_mods & GDK_MOD1_MASK) ? ~GDK_MOD1_MASK : ~GDK_CONTROL_MASK;
21		if (!gtk_accel_map_change_entry(accel_path,accel_key,accel_mods,FALSE)) {
22		g_print("could not change accelerator %s\n",accel_path);
23		}
24		}
25		if (accel_mods & GDK_MOD1_MASK) {
26		accel_mods &= ~ GDK_MOD1_MASK;
27		accel_mods \|= GDK_CONTROL_MASK;
28		if (!gtk_accel_map_change_entry(accel_path,accel_key,accel_mods,FALSE)) {
29		g_print("could not change accelerator %s\n",accel_path);
30		}
31		}
32		}
33
34		static gboolean deal_with_open(GtkOSXApplication app, gchar path, gpointer user_data)
35		{
36		CAMLparam0();
37		CAMLlocal2(string_path, res);
38		string_path = caml_copy_string(path);
39		res = caml_callback_exn(open_file_fun,string_path);
40		gboolean truc = !(Is_exception_result(res));
41		CAMLreturnT(gboolean, truc);
42		}
43
44		static gboolean deal_with_quit(GtkOSXApplication *app, gpointer user_data)
45		{
46		CAMLparam0();
47		CAMLlocal1(res);
48		res = caml_callback_exn(forbid_quit_fun,Val_unit);
49		gboolean truc = (Bool_val(res))\|\|((Is_exception_result(res)));
50		CAMLreturnT(gboolean, truc);
51		}
52
53		CAMLprim value caml_gtk_mac_init(value open_file_the_fun, value forbid_quit_the_fun)
54		{
55		CAMLparam2(open_file_the_fun,forbid_quit_the_fun);
56		open_file_fun = open_file_the_fun;
57		caml_register_generational_global_root(&open_file_fun);
58		forbid_quit_fun = forbid_quit_the_fun;
59		caml_register_generational_global_root(&forbid_quit_fun);
60		theApp = g_object_new(GTK_TYPE_OSX_APPLICATION, NULL);
61		g_signal_connect(theApp, "NSApplicationOpenFile", G_CALLBACK(deal_with_open), NULL);
62		g_signal_connect(theApp, "NSApplicationBlockTermination", G_CALLBACK(deal_with_quit), NULL);
63		CAMLreturn (Val_unit);
64		}
65
66		CAMLprim value caml_gtk_mac_ready(value menubar, value prefs, value about)
67		{
68		GtkOSXApplicationMenuGroup * pref_grp, * about_grp;
69		CAMLparam3(menubar,prefs,about);
70		themenubar = menubar;
71		pref_item = prefs;
72		about_item = about;
73		caml_register_generational_global_root(&themenubar);
74		caml_register_generational_global_root(&pref_item);
75		caml_register_generational_global_root(&about_item);
76		/* gtk_accel_map_foreach(NULL, osx_accel_map_foreach_lcb);*/
77		gtk_osxapplication_set_menu_bar(theApp,check_cast(GTK_MENU_SHELL,themenubar));
78		gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,about_item),1);
79		gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),2);
80		gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,pref_item),3);
81		gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),4);
82		gtk_osxapplication_ready(theApp);
83		CAMLreturn(Val_unit);
84		}

+4

-0

ide/preferences.ml less more

34	34	\| `MOD5 -> "<Mod5>"
35	35	\| `CONTROL -> "<Control>"
36	36	\| `SHIFT -> "<Shift>"
	37	\| `HYPER -> "<Hyper>"
	38	\| `META -> "<Meta>"
	39	\| `RELEASE -> ""
	40	\| `SUPER -> "<Super>"
37	41	\| `BUTTON1\| `BUTTON2\| `BUTTON3\| `BUTTON4\| `BUTTON5\| `LOCK -> ""
38	42
39	43	let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l

+9

-1

ide/utils/okey.ml less more

46	46	\| `BUTTON3 -> 1024
47	47	\| `BUTTON4 -> 2048
48	48	\| `BUTTON5 -> 4096
	49	\| `HYPER -> 1 lsl 22
	50	\| `META -> 1 lsl 20
	51	\| `RELEASE -> 1 lsl 30
	52	\| `SUPER -> 1 lsl 21
49	53
50	54	let print_modifier l =
51	55	List.iter

64	68	\| `BUTTON2 -> "B2"
65	69	\| `BUTTON3 -> "B3"
66	70	\| `BUTTON4 -> "B4"
67		\| `BUTTON5 -> "B5")
	71	\| `BUTTON5 -> "B5"
	72	\| `HYPER -> "HYPER"
	73	\| `META -> "META"
	74	\| `RELEASE -> ""
	75	\| `SUPER -> "SUPER")
68	76	m)^" ")
69	77	)
70	78	l;

+7

-4

interp/constrextern.ml less more

249	249	check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
250	250	\| _ -> failwith "not same binder") bl1 bl2
251	251
252		let is_same_type c d = try let () = check_same_type c d in true with Failure _ -> false
	252	let is_same_type c d =
	253	try let () = check_same_type c d in true
	254	with Failure _ \| Invalid_argument _ -> false
253	255
254	256	(**********************************************************************)
255	257	(* mapping patterns to cases_pattern_expr *)

373	375	\| (keyrule,pat,n as _rule)::rules ->
374	376	try
375	377	match t,n with
376		\| PatCstr (loc,(ind,_),l,na), n when n = Some 0 or n = None or
377		n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams ->
	378	\| PatCstr (loc,(ind,_),l,na), n when (n = Some 0 or n = None or
	379	n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams)
	380	&& (match keyrule with SynDefRule _ -> true \| _ -> false) ->
378	381	(* Abbreviation for the constructor name only *)
379	382	(match keyrule with
380		\| NotationRule (sc,ntn) -> raise No_match
	383	\| NotationRule _ -> assert false
381	384	\| SynDefRule kn ->
382	385	let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
383	386	let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in

+2

-1

interp/constrintern.ml less more

1410	1410	\| None ->
1411	1411	[], None in
1412	1412	let na = match tm', na with
1413		\| GVar (loc,id), None when Idset.mem id env.ids -> loc,Name id
	1413	\| GVar (loc,id), None when not (List.mem_assoc id (snd lvar)) ->
	1414	loc,Name id
1414	1415	\| GRef (loc, VarRef id), None -> loc,Name id
1415	1416	\| _, None -> dummy_loc,Anonymous
1416	1417	\| _, Some (loc,na) -> loc,na in

+50

-22

kernel/univ.ml less more

124	124
125	125	(* Comparison on this type is pointer equality *)
126	126	type canonical_arc =
127		{ univ: UniverseLevel.t; lt: UniverseLevel.t list; le: UniverseLevel.t list }
128
129		let terminal u = {univ=u; lt=[]; le=[]}
	127	{ univ: UniverseLevel.t;
	128	lt: UniverseLevel.t list;
	129	le: UniverseLevel.t list;
	130	rank: int }
	131
	132	let terminal u = {univ=u; lt=[]; le=[]; rank=0}
130	133
131	134	(* A UniverseLevel.t is either an alias for another one, or a canonical one,
132	135	for which we know the universes that are above *)

404	407	(* we assume compare(u,v) = LE *)
405	408	(* merge u v forces u ~ v with repr u as canonical repr *)
406	409	let merge g arcu arcv =
407		match between g arcu arcv with
408		\| arcu::v -> (* arcu is chosen as canonical and all others (v) are *)
409		(* redirected to it *)
410		let redirect (g,w,w') arcv =
411		let g' = enter_equiv_arc arcv.univ arcu.univ g in
412		(g',list_unionq arcv.lt w,arcv.le@w')
413		in
414		let (g',w,w') = List.fold_left redirect (g,[],[]) v in
415		let g_arcu = (g',arcu) in
416		let g_arcu = List.fold_left setlt_if g_arcu w in
417		let g_arcu = List.fold_left setleq_if g_arcu w' in
418		fst g_arcu
419		\| [] -> anomaly "Univ.between"
	410	(* we find the arc with the biggest rank, and we redirect all others to it *)
	411	let arcu, g, v =
	412	let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
	413	if arc.rank >= max_rank
	414	then (arc.rank, max_rank, arc, best_arc::rest)
	415	else (max_rank, old_max_rank, best_arc, arc::rest)
	416	in
	417	match between g arcu arcv with
	418	\| [] -> anomaly "Univ.between"
	419	\| arc::rest ->
	420	let (max_rank, old_max_rank, best_arc, rest) =
	421	List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
	422	if max_rank > old_max_rank then best_arc, g, rest
	423	else begin
	424	(* one redirected node also has max_rank *)
	425	let arcu = {best_arc with rank = max_rank + 1} in
	426	arcu, enter_arc arcu g, rest
	427	end
	428	in
	429	let redirect (g,w,w') arcv =
	430	let g' = enter_equiv_arc arcv.univ arcu.univ g in
	431	(g',list_unionq arcv.lt w,arcv.le@w')
	432	in
	433	let (g',w,w') = List.fold_left redirect (g,[],[]) v in
	434	let g_arcu = (g',arcu) in
	435	let g_arcu = List.fold_left setlt_if g_arcu w in
	436	let g_arcu = List.fold_left setleq_if g_arcu w' in
	437	fst g_arcu
420	438
421	439	(* merge_disc : UniverseLevel.t -> UniverseLevel.t -> unit *)
422	440	(* we assume compare(u,v) = compare(v,u) = NLE *)
423	441	(* merge_disc u v forces u ~ v with repr u as canonical repr *)
424		let merge_disc g arcu arcv =
	442	let merge_disc g arc1 arc2 =
	443	let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
	444	let arcu, g =
	445	if arc1.rank <> arc2.rank then arcu, g
	446	else
	447	let arcu = {arcu with rank = succ arcu.rank} in
	448	arcu, enter_arc arcu g
	449	in
425	450	let g' = enter_equiv_arc arcv.univ arcu.univ g in
426	451	let g_arcu = (g',arcu) in
427	452	let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in

562	587	in
563	588	let canonicalize u = function
564	589	\| Equiv _ -> Equiv (repr u)
565		\| Canonical {univ=v; lt=lt; le=le} ->
	590	\| Canonical {univ=v; lt=lt; le=le; rank=rank} ->
566	591	assert (u == v);
567	592	(* avoid duplicates and self-loops *)
568	593	let lt = lrepr lt and le = lrepr le in

574	599	univ = v;
575	600	lt = UniverseLSet.elements lt;
576	601	le = UniverseLSet.elements le;
	602	rank = rank
577	603	}
578	604	in
579	605	UniverseLMap.mapi canonicalize g

631	657	let node = Canonical {
632	658	univ = bottom;
633	659	lt = [];
634		le = UniverseLSet.elements vertices
	660	le = UniverseLSet.elements vertices;
	661	rank = 0
635	662	} in UniverseLMap.add bottom node g
636	663	in
637	664	let rec iter count accu =

691	718	\| false, true -> push res v
692	719	\| false, false -> res
693	720	end
694		\| Canonical {univ=v; lt=lt; le=le} ->
	721	\| Canonical {univ=v; lt=lt; le=le; rank=r} ->
695	722	assert (u == v);
696	723	if filter u then
697	724	let lt = List.filter filter lt in
698	725	let le = List.filter filter le in
699		UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le}) res
	726	UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le; rank=r}) res
700	727	else
701	728	let res = List.fold_left (fun g u -> if filter u then push g u else g) res lt in
702	729	let res = List.fold_left (fun g u -> if filter u then push g u else g) res le in

716	743	let g = UniverseLMap.add u (Canonical {
717	744	univ = u;
718	745	le = [];
719		lt = [types.(i+1)]
	746	lt = [types.(i+1)];
	747	rank = 1
720	748	}) g in aux (i+1) g
721	749	else g
722	750	in aux 0 g

+18

-19

lib/xml_parser.ml less more

41	41	\| AttributeValueExpected
42	42	\| EndOfTagExpected of string
43	43	\| EOFExpected
	44	\| Empty
44	45
45	46	type error = error_msg * error_pos
46	47

116	117	\| Xml_lexer.PCData s -> PCData s
117	118	\| Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, [])
118	119	\| Xml_lexer.Tag (tag, attr, false) ->
119		let elements = read_elems ~tag s in
	120	let elements = read_elems tag s in
120	121	Element (tag, attr, canonicalize elements)
121	122	\| t ->
122	123	push t s;
123	124	raise NoMoreData
124	125	and
125		read_elems ?tag s =
	126	read_elems tag s =
126	127	let elems = ref [] in
127	128	(try
128	129	while true do

136	137	with
137	138	NoMoreData -> ());
138	139	match pop s with
139		\| Xml_lexer.Endtag s when Some s = tag -> List.rev !elems
140		\| Xml_lexer.Eof when tag = None -> List.rev !elems
141		\| t ->
142		match tag with
143		\| None -> raise (Internal_error EOFExpected)
144		\| Some s -> raise (Internal_error (EndOfTagExpected s))
	140	\| Xml_lexer.Endtag s when s = tag -> List.rev !elems
	141	\| t -> raise (Internal_error (EndOfTagExpected tag))
145	142
146	143	let rec read_xml s =
147	144	let node = read_node s in

161	158	\| Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
162	159	\| Xml_lexer.EUnterminatedEntity -> UnterminatedEntity
163	160
	161	let error_of_exn stk = function
	162	\| NoMoreData when Stack.pop stk = Xml_lexer.Eof -> Empty
	163	\| NoMoreData -> NodeExpected
	164	\| Internal_error e -> e
	165	\| Xml_lexer.Error e -> convert e
	166	\| e -> raise e
	167
164	168	let do_parse xparser source =
	169	let stk = Stack.create() in
165	170	try
166	171	Xml_lexer.init source;
167		let s = { source = source; xparser = xparser; stack = Stack.create(); } in
	172	let s = { source = source; xparser = xparser; stack = stk } in
168	173	let x = read_xml s in
169	174	if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
170	175	Xml_lexer.close source;
171	176	x
172		with
173		\| NoMoreData ->
174		Xml_lexer.close source;
175		raise (!xml_error NodeExpected source)
176		\| Internal_error e ->
177		Xml_lexer.close source;
178		raise (!xml_error e source)
179		\| Xml_lexer.Error e ->
180		Xml_lexer.close source;
181		raise (!xml_error (convert e) source)
	177	with e ->
	178	Xml_lexer.close source;
	179	raise (!xml_error (error_of_exn stk e) source)
182	180
183	181	let parse p = function
184	182	\| SChannel ch -> do_parse p (Lexing.from_channel ch)

207	205	\| AttributeValueExpected -> "Attribute value expected"
208	206	\| EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag
209	207	\| EOFExpected -> "End of file expected"
	208	\| Empty -> "Empty"
210	209
211	210	let error (msg,pos) =
212	211	if pos.emin = pos.emax then

+1

-0

lib/xml_parser.mli less more

58	58	\| AttributeValueExpected
59	59	\| EndOfTagExpected of string
60	60	\| EOFExpected
	61	\| Empty
61	62
62	63	type error = error_msg * error_pos
63	64

+2

-2

myocamlbuild.ml less more

421	421	if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico])
422	422	in
423	423	if opt then rule fo ~prod:fo ~deps:(depsall@depso) ~insert:`top
424		(cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;A"-o";Px fo]);
	424	(cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;camlp4incl;A"-o";Px fo]);
425	425	rule fb ~prod:fb ~deps:(depsall@depsb) ~insert:`top
426		(cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;A"-o";Px fb]);
	426	(cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;camlp4incl;A"-o";Px fb]);
427	427	in
428	428
429	429	(** Coq files dependencies *)

+12

-5

parsing/pptactic.ml less more

259	259
260	260	let rec tacarg_using_rule_token pr_gen = function
261	261	\| Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
262		\| None :: l, a :: al -> pr_gen a :: tacarg_using_rule_token pr_gen (l,al)
	262	\| None :: l, a :: al ->
	263	let print_it =
	264	match genarg_tag a with
	265	\| OptArgType _ -> fold_opt (fun _ -> true) false a
	266	\| _ -> true
	267	in
	268	let r = tacarg_using_rule_token pr_gen (l,al) in
	269	if print_it then pr_gen a :: r else r
263	270	\| [], [] -> []
264	271	\| _ -> failwith "Inconsistent arguments of extended tactic"
265	272

422	429	(if occs = no_occurrences_expr then mt ()
423	430	else pr_with_occurrences (fun () -> str" \|- *") (occs,())))
424	431
425		let pr_orient b = if b then mt () else str " <-"
	432	let pr_orient b = if b then mt () else str "<- "
426	433
427	434	let pr_multi = function
428	435	\| Precisely 1 -> mt ()

805	812
806	813	(* Equivalence relations *)
807	814	\| TacReflexivity as x -> pr_atom0 x
808		\| TacSymmetry cls -> str "symmetry " ++ pr_clauses (Some true) pr_ident cls
	815	\| TacSymmetry cls -> str "symmetry" ++ pr_clauses (Some true) pr_ident cls
809	816	\| TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c
810	817	\| TacTransitivity None -> str "etransitivity"
811	818
812	819	(* Equality and inversion *)
813	820	\| TacRewrite (ev,l,cl,by) ->
814		hov 1 (str (with_evars ev "rewrite") ++
	821	hov 1 (str (with_evars ev "rewrite") ++ spc () ++
815	822	prlist_with_sep
816	823	(fun () -> str ","++spc())
817	824	(fun (b,m,c) ->
818		pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c)
	825	pr_orient b ++ pr_multi m ++ pr_with_bindings c)
819	826	l
820	827	++ pr_clauses (Some true) pr_ident cl
821	828	++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by \| None -> mt()))

+9

-5

plugins/extraction/ExtrOcamlNatInt.v less more

12	12
13	13	(** Disclaimer: trying to obtain efficient certified programs
14	14	by extracting [nat] into [int] is definitively not a good idea:
	15
	16	- This is just a syntactic adaptation, many things can go wrong,
	17	such as name captures (e.g. if you have a constant named "int"
	18	in your development, or a module named "Pervasives"). See bug #2878.
15	19
16	20	- Since [int] is bounded while [nat] is (theoretically) infinite,
17	21	you have to make sure by yourself that your program will not

33	37	(** Mapping of [nat] into [int]. The last string corresponds to
34	38	a [nat_case], see documentation of [Extract Inductive]. *)
35	39
36		Extract Inductive nat => int [ "0" "succ" ]
	40	Extract Inductive nat => int [ "0" "Pervasives.succ" ]
37	41	"(fun fO fS n -> if n=0 then fO () else fS (n-1))".
38	42
39	43	(** Efficient (but uncertified) versions for usual [nat] functions *)
40	44
41	45	Extract Constant plus => "(+)".
42		Extract Constant pred => "fun n -> max 0 (n-1)".
43		Extract Constant minus => "fun n m -> max 0 (n-m)".
	46	Extract Constant pred => "fun n -> Pervasives.max 0 (n-1)".
	47	Extract Constant minus => "fun n m -> Pervasives.max 0 (n-m)".
44	48	Extract Constant mult => "( * )".
45		Extract Inlined Constant max => max.
46		Extract Inlined Constant min => min.
	49	Extract Inlined Constant max => "Pervasives.max".
	50	Extract Inlined Constant min => "Pervasives.min".
47	51	(Extract Inlined Constant nat_beq => "(=)".)
48	52	Extract Inlined Constant EqNat.beq_nat => "(=)".
49	53	Extract Inlined Constant EqNat.eq_nat_decide => "(=)".

+16

-16

plugins/extraction/ExtrOcamlZInt.v less more

33	33	(** Efficient (but uncertified) versions for usual functions *)
34	34
35	35	Extract Constant Pos.add => "(+)".
36		Extract Constant Pos.succ => "succ".
37		Extract Constant Pos.pred => "fun n -> max 1 (n-1)".
38		Extract Constant Pos.sub => "fun n m -> max 1 (n-m)".
	36	Extract Constant Pos.succ => "Pervasives.succ".
	37	Extract Constant Pos.pred => "fun n -> Pervasives.max 1 (n-1)".
	38	Extract Constant Pos.sub => "fun n m -> Pervasives.max 1 (n-m)".
39	39	Extract Constant Pos.mul => "( * )".
40		Extract Constant Pos.min => "min".
41		Extract Constant Pos.max => "max".
	40	Extract Constant Pos.min => "Pervasives.min".
	41	Extract Constant Pos.max => "Pervasives.max".
42	42	Extract Constant Pos.compare =>
43	43	"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
44	44	Extract Constant Pos.compare_cont =>

46	46
47	47
48	48	Extract Constant N.add => "(+)".
49		Extract Constant N.succ => "succ".
50		Extract Constant N.pred => "fun n -> max 0 (n-1)".
51		Extract Constant N.sub => "fun n m -> max 0 (n-m)".
	49	Extract Constant N.succ => "Pervasives.succ".
	50	Extract Constant N.pred => "fun n -> Pervasives.max 0 (n-1)".
	51	Extract Constant N.sub => "fun n m -> Pervasives.max 0 (n-m)".
52	52	Extract Constant N.mul => "( * )".
53		Extract Constant N.min => "min".
54		Extract Constant N.max => "max".
	53	Extract Constant N.min => "Pervasives.min".
	54	Extract Constant N.max => "Pervasives.max".
55	55	Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b".
56	56	Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b".
57	57	Extract Constant N.compare =>

59	59
60	60
61	61	Extract Constant Z.add => "(+)".
62		Extract Constant Z.succ => "succ".
63		Extract Constant Z.pred => "pred".
	62	Extract Constant Z.succ => "Pervasives.succ".
	63	Extract Constant Z.pred => "Pervasives.pred".
64	64	Extract Constant Z.sub => "(-)".
65	65	Extract Constant Z.mul => "( * )".
66	66	Extract Constant Z.opp => "(~-)".
67		Extract Constant Z.abs => "abs".
68		Extract Constant Z.min => "min".
69		Extract Constant Z.max => "max".
	67	Extract Constant Z.abs => "Pervasives.abs".
	68	Extract Constant Z.min => "Pervasives.min".
	69	Extract Constant Z.max => "Pervasives.max".
70	70	Extract Constant Z.compare =>
71	71	"fun x y -> if x=y then Eq else if x<y then Lt else Gt".
72	72
73	73	Extract Constant Z.of_N => "fun p -> p".
74		Extract Constant Z.abs_N => "abs".
	74	Extract Constant Z.abs_N => "Pervasives.abs".
75	75
76	76	(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod).
77	77	For the moment we don't even try *)

+26

-10

plugins/extraction/extraction.ml less more

129	129
130	130	(* Enriching a signature with implicit information *)
131	131
132		let sign_with_implicits r s =
	132	let sign_with_implicits r s nb_params =
133	133	let implicits = implicits_of_global r in
134	134	let rec add_impl i = function
135	135	\| [] -> []

138	138	if sign = Keep && List.mem i implicits then Kill Kother else sign
139	139	in sign' :: add_impl (succ i) s
140	140	in
141		add_impl 1 s
	141	add_impl (1+nb_params) s
142	142
143	143	(* Enriching a exception message *)
144	144

666	666	let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
667	667	(* Now, the extraction of the arguments. *)
668	668	let s_full = type2signature env (snd schema) in
669		let s_full = sign_with_implicits (ConstRef kn) s_full in
	669	let s_full = sign_with_implicits (ConstRef kn) s_full 0 in
670	670	let s = sign_no_final_keeps s_full in
671	671	let ls = List.length s in
672	672	let la = List.length args in
673	673	(* The ml arguments, already expunged from known logical ones *)
674	674	let mla = make_mlargs env mle s args metas in
675	675	let mla =
676		if not magic1 then
	676	if magic1 \|\| lang () <> Ocaml then mla
	677	else
677	678	try
	679	(* for better optimisations later, we discard dependent args
	680	of projections and replace them by fake args that will be
	681	removed during final pretty-print. *)
678	682	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
679	683	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
680	684	else mla
681	685	with _ -> mla
682		else mla
683	686	in
684	687	(* For strict languages, purely logical signatures with at least
685	688	one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left

725	728	let type_cons = instantiation (nb_tvars, type_cons) in
726	729	(* Then, the usual variables [s], [ls], [la], ... *)
727	730	let s = List.map (type2sign env) types in
728		let s = sign_with_implicits (ConstructRef cp) s in
	731	let s = sign_with_implicits (ConstructRef cp) s params_nb in
729	732	let ls = List.length s in
730	733	let la = List.length args in
731	734	assert (la <= ls + params_nb);

804	807	let l = List.map f oi.ip_types.(i) in
805	808	(* the corresponding signature *)
806	809	let s = List.map (type2sign env) oi.ip_types.(i) in
807		let s = sign_with_implicits r s in
	810	let s = sign_with_implicits r s mi.ind_nparams in
808	811	(* Extraction of the branch (in functional form). *)
809	812	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
810	813	(* We suppress dummy arguments according to signature. *)

875	878	let l,t' = type_decomp (expand env (var2var' t)) in
876	879	let s = List.map (type2sign env) l in
877	880	(* Check for user-declared implicit information *)
878		let s = sign_with_implicits (ConstRef kn) s in
	881	let s = sign_with_implicits (ConstRef kn) s 0 in
879	882	(* Decomposing the top level lambdas of [body].
880	883	If there isn't enough, it's ok, as long as remaining args
881	884	aren't to be pruned (and initial lambdas aren't to be all

921	924	let trm = handle_exn (ConstRef kn) n (fun i -> fst (List.nth rels (i-1))) trm
922	925	in
923	926	trm, type_expunge_from_sign env s t
	927
	928	(* Extracts the type of an axiom, honors the Extraction Implicit declaration. *)
	929	let extract_axiom env kn typ =
	930	reset_meta_count ();
	931	(* The short type [t] (i.e. possibly with abbreviations). *)
	932	let t = snd (record_constant_type env kn (Some typ)) in
	933	(* The real type [t']: without head products, expanded, *)
	934	(* and with [Tvar] translated to [Tvar'] (not instantiable). *)
	935	let l,_ = type_decomp (expand env (var2var' t)) in
	936	let s = List.map (type2sign env) l in
	937	(* Check for user-declared implicit information *)
	938	let s = sign_with_implicits (ConstRef kn) s 0 in
	939	type_expunge_from_sign env s t
924	940
925	941	let extract_fixpoint env vkn (fi,ti,ci) =
926	942	let n = Array.length vkn in

958	974	in Dtype (r, vl, t)
959	975	in
960	976	let mk_ax () =
961		let t = snd (record_constant_type env kn (Some typ)) in
962		Dterm (r, MLaxiom, type_expunge env t)
	977	let t = extract_axiom env kn typ in
	978	Dterm (r, MLaxiom, t)
963	979	in
964	980	let mk_def c =
965	981	let e,t = extract_std_constant env kn c typ in

+33

-27

plugins/extraction/modutil.ml less more

25	25	(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
26	26	[ml_structure]. *)
27	27
28		let se_iter do_decl do_spec =
	28	let se_iter do_decl do_spec do_mp =
29	29	let rec mt_iter = function
30		\| MTident _ -> ()
	30	\| MTident mp -> do_mp mp
31	31	\| MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
32	32	\| MTwith (mt,ML_With_type(idl,l,t))->
33	33	let mp_mt = msid_of_mt mt in

37	37	in
38	38	let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
39	39	mt_iter mt; do_decl (Dtype(r,l,t))
40		\| MTwith (mt,_)->mt_iter mt
	40	\| MTwith (mt,ML_With_module(idl,mp))->
	41	let mp_mt = msid_of_mt mt in
	42	let mp_w =
	43	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl
	44	in
	45	mt_iter mt; do_mp mp_w; do_mp mp
41	46	\| MTsig (_, sign) -> List.iter spec_iter sign
42	47	and spec_iter = function
43	48	\| (_,Spec s) -> do_spec s

50	55	me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
51	56	\| (_,SEmodtype m) -> mt_iter m
52	57	and me_iter = function
53		\| MEident _ -> ()
	58	\| MEident mp -> do_mp mp
54	59	\| MEfunctor (_,mt,me) -> me_iter me; mt_iter mt
55	60	\| MEapply (me,me') -> me_iter me; me_iter me'
56	61	\| MEstruct (msid, sel) -> List.iter se_iter sel
57	62	in
58	63	se_iter
59	64
60		let struct_iter do_decl do_spec s =
61		List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s
	65	let struct_iter do_decl do_spec do_mp s =
	66	List.iter
	67	(function (_,sel) -> List.iter (se_iter do_decl do_spec do_mp) sel) s
62	68
63	69	(*s Apply some fonctions upon all references in [ml_type], [ml_ast],
64	70	[ml_decl], [ml_spec] and [ml_structure]. *)

140	146	\| _ -> ()
141	147
142	148	let struct_ast_search f s =
143		try struct_iter (decl_ast_search f) (fun _ -> ()) s; false
	149	try struct_iter (decl_ast_search f) (fun _ -> ()) (fun _ -> ()) s; false
144	150	with Found -> true
145	151
146	152	let rec type_search f = function

164	170	\| Sval (_,u) -> type_search f u
165	171
166	172	let struct_type_search f s =
167		try struct_iter (decl_type_search f) (spec_type_search f) s; false
	173	try
	174	struct_iter (decl_type_search f) (spec_type_search f) (fun _ -> ()) s;
	175	false
168	176	with Found -> true
169	177
170	178

246	254	let c = Array.map (subst 0) av
247	255	in MLfix(i, ids, c)
248	256
	257	(* [optim_se] applies the [normalize] function everywhere and does the
	258	inlining of code. The inlined functions are kept for the moment in
	259	order to preserve the global interface, later [depcheck_se] will get
	260	rid of them if possible *)
	261
249	262	let rec optim_se top to_appear s = function
250	263	\| [] -> []
251	264	\| (l,SEdecl (Dterm (r,a,t))) :: lse ->
252	265	let a = normalize (ast_glob_subst !s a) in
253	266	let i = inline r a in
254	267	if i then s := Refmap'.add r a !s;
255		if top && i && not (library ()) && not (List.mem r to_appear)
256		then optim_se top to_appear s lse
257		else
258		let d = match optimize_fix a with
259		\| MLfix (0, _, [\|c\|]) ->
260		Dfix ([\|r\|], [\|ast_subst (MLglob r) c\|], [\|t\|])
261		\| a -> Dterm (r, a, t)
262		in (l,SEdecl d) :: (optim_se top to_appear s lse)
	268	let d = match optimize_fix a with
	269	\| MLfix (0, _, [\|c\|]) ->
	270	Dfix ([\|r\|], [\|ast_subst (MLglob r) c\|], [\|t\|])
	271	\| a -> Dterm (r, a, t)
	272	in
	273	(l,SEdecl d) :: (optim_se top to_appear s lse)
263	274	\| (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
264	275	let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
265		let all = ref true in
266	276	(* This fake body ensures that no fixpoint will be auto-inlined. *)
267	277	let fake_body = MLfix (0,[\|\|],[\|\|]) in
268	278	for i = 0 to Array.length rv - 1 do
269	279	if inline rv.(i) fake_body
270	280	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
271		else all := false
272	281	done;
273		if !all && top && not (library ())
274		&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)
275		then optim_se top to_appear s lse
276		else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
	282	(l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
277	283	\| (l,SEmodule m) :: lse ->
278	284	let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
279	285	in (l,SEmodule m) :: (optim_se top to_appear s lse)

288	294
289	295	(* After these optimisations, some dependencies may not be needed anymore.
290	296	For non-library extraction, we recompute a minimal set of dependencies
291		for first-level objects *)
	297	for first-level definitions (no module pruning yet). *)
292	298
293	299	exception NoDepCheck
294	300

361	367	end
362	368	\| t :: se ->
363	369	let se' = depcheck_se se in
364		se_iter compute_deps_decl compute_deps_spec t;
	370	se_iter compute_deps_decl compute_deps_spec add_needed_mp t;
365	371	t :: se'
366	372
367	373	let rec depcheck_struct = function

369	375	\| (mp,lse)::struc ->
370	376	let struc' = depcheck_struct struc in
371	377	let lse' = depcheck_se lse in
372		(mp,lse')::struc'
	378	if lse' = [] then struc' else (mp,lse')::struc'
373	379
374	380	let check_implicits = function
375	381	\| MLexn s ->

388	394	List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse))
389	395	struc
390	396	in
391		let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
392	397	ignore (struct_ast_search check_implicits opt_struc);
393		if library () then opt_struc
	398	if library () then
	399	List.filter (fun (_,lse) -> lse<>[]) opt_struc
394	400	else begin
395	401	reset_needed ();
396	402	List.iter add_needed (fst to_appear);

+9

-8

plugins/funind/glob_term_to_relation.ml less more

307	307	(Global.env ())
308	308	construct
309	309	in
310		let argl =
311		if argl = []
312		then
	310	let argl = match argl with
	311	\| None ->
313	312	Array.to_list
314		(Array.init (cst_narg - npar) (fun _ -> mkGHole ())
	313	(Array.init cst_narg (fun _ -> mkGHole ())
315	314	)
316		else argl
	315	\| Some l ->
	316	Array.to_list
	317	(Array.init npar (fun _ -> mkGHole ()))@l
317	318	in
318	319	let pat_as_term =
319	320	mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)

652	653	Printer.pr_glob_constr b ++ str " in " ++
653	654	Printer.pr_glob_constr rt ++ str ". try again with a cast")
654	655	in
655		let case_pats = build_constructors_of_type ind [] in
	656	let case_pats = build_constructors_of_type ind None in
656	657	assert (Array.length case_pats = 2);
657	658	let brl =
658	659	list_map_i

668	669	\| GLetTuple(_,nal,_,b,e) ->
669	670	begin
670	671	let nal_as_glob_constr =
671		List.map
	672	Some (List.map
672	673	(function
673	674	Name id -> mkGVar id
674	675	\| Anonymous -> mkGHole ()
675	676	)
676		nal
	677	nal)
677	678	in
678	679	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
679	680	let b_typ = Typing.type_of env Evd.empty b_as_constr in

+48

-77

plugins/romega/ReflOmegaCore.v less more

13	13
14	14	Module Type Int.
15	15
16		Parameter int : Set.
17
18		Parameter zero : int.
19		Parameter one : int.
20		Parameter plus : int -> int -> int.
21		Parameter opp : int -> int.
22		Parameter minus : int -> int -> int.
23		Parameter mult : int -> int -> int.
	16	Parameter t : Set.
	17
	18	Parameter zero : t.
	19	Parameter one : t.
	20	Parameter plus : t -> t -> t.
	21	Parameter opp : t -> t.
	22	Parameter minus : t -> t -> t.
	23	Parameter mult : t -> t -> t.
24	24
25	25	Notation "0" := zero : Int_scope.
26	26	Notation "1" := one : Int_scope.

32	32	Open Scope Int_scope.
33	33
34	34	(* First, int is a ring: *)
35		Axiom ring : @ring_theory int 0 1 plus mult minus opp (@eq int).
	35	Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t).
36	36
37	37	(* int should also be ordered: *)
38	38
39		Parameter le : int -> int -> Prop.
40		Parameter lt : int -> int -> Prop.
41		Parameter ge : int -> int -> Prop.
42		Parameter gt : int -> int -> Prop.
	39	Parameter le : t -> t -> Prop.
	40	Parameter lt : t -> t -> Prop.
	41	Parameter ge : t -> t -> Prop.
	42	Parameter gt : t -> t -> Prop.
43	43	Notation "x <= y" := (le x y): Int_scope.
44	44	Notation "x < y" := (lt x y) : Int_scope.
45	45	Notation "x >= y" := (ge x y) : Int_scope.

60	60	forall i j k, 0 < k -> i < j -> ki<kj.
61	61
62	62	(* We should have a way to decide the equality and the order*)
63		Parameter compare : int -> int -> comparison.
	63	Parameter compare : t -> t -> comparison.
64	64	Infix "?=" := compare (at level 70, no associativity) : Int_scope.
65	65	Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j.
66	66	Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j.

82	82
83	83	Open Scope Z_scope.
84	84
85		Definition int := Z.
	85	Definition t := Z.
86	86	Definition zero := 0.
87	87	Definition one := 1.
88	88	Definition plus := Z.add.

90	90	Definition minus := Z.sub.
91	91	Definition mult := Z.mul.
92	92
93		Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int).
	93	Lemma ring : @ring_theory t zero one plus mult minus opp (@eq t).
94	94	Proof.
95	95	constructor.
96	96	exact Z.add_0_l.

137	137
138	138	Module IntProperties (I:Int).
139	139	Import I.
	140	Local Notation int := I.t.
140	141
141	142	(* Primo, some consequences of being a ring theory... *)
142	143

826	827	Import I.
827	828	Module IP:=IntProperties(I).
828	829	Import IP.
	830	Local Notation int := I.t.
829	831
830	832	(* \subsubsection{Definition of reified integer expressions}
831	833	Terms are either:

1036	1038
1037	1039	Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.
1038	1040	Proof.
1039		simple induction t1; intros until t2; case t2; simpl in *;
1040		try (intros; discriminate; fail);
1041		[ intros; elim beq_true with (1 := H); trivial
1042		\| intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
1043		elim H with (1 := H4); elim H0 with (1 := H5);
1044		trivial
1045		\| intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
1046		elim H with (1 := H4); elim H0 with (1 := H5);
1047		trivial
1048		\| intros t21 t22 H3; elim andb_prop with (1 := H3); intros H4 H5;
1049		elim H with (1 := H4); elim H0 with (1 := H5);
1050		trivial
1051		\| intros t21 H3; elim H with (1 := H3); trivial
1052		\| intros; elim beq_nat_true with (1 := H); trivial ].
	1041	induction t1; destruct t2; simpl in *; try discriminate;
	1042	(rewrite andb_true_iff; intros (H1,H2)) \|\| intros H; f_equal;
	1043	auto using beq_true, beq_nat_true.
	1044	Qed.
	1045
	1046	Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true.
	1047	Proof.
	1048	induction t0; simpl in *; try (apply andb_true_iff; split); trivial.
	1049	- now apply beq_iff.
	1050	- now apply beq_nat_true_iff.
1053	1051	Qed.
1054	1052
1055	1053	Ltac trivial_case := unfold not; intros; discriminate.

1057	1055	Theorem eq_term_false :
1058	1056	forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.
1059	1057	Proof.
1060		simple induction t1;
1061		[ intros z t2; case t2; try trivial_case; simpl; unfold not;
1062		intros; elim beq_false with (1 := H); simplify_eq H0;
1063		auto
1064		\| intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
1065		intros t21 t22 H3; unfold not; intro H4;
1066		elim andb_false_elim with (1 := H3); intros H5;
1067		[ elim H1 with (1 := H5); simplify_eq H4; auto
1068		\| elim H2 with (1 := H5); simplify_eq H4; auto ]
1069		\| intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
1070		intros t21 t22 H3; unfold not; intro H4;
1071		elim andb_false_elim with (1 := H3); intros H5;
1072		[ elim H1 with (1 := H5); simplify_eq H4; auto
1073		\| elim H2 with (1 := H5); simplify_eq H4; auto ]
1074		\| intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl;
1075		intros t21 t22 H3; unfold not; intro H4;
1076		elim andb_false_elim with (1 := H3); intros H5;
1077		[ elim H1 with (1 := H5); simplify_eq H4; auto
1078		\| elim H2 with (1 := H5); simplify_eq H4; auto ]
1079		\| intros t11 H1 t2; case t2; try trivial_case; simpl; intros t21 H3;
1080		unfold not; intro H4; elim H1 with (1 := H3);
1081		simplify_eq H4; auto
1082		\| intros n t2; case t2; try trivial_case; simpl; unfold not;
1083		intros; elim beq_nat_false with (1 := H); simplify_eq H0;
1084		auto ].
	1058	intros t1 t2 H E. subst t2. now rewrite eq_term_refl in H.
1085	1059	Qed.
1086	1060
1087	1061	(* \subsubsection{Tactiques pour éliminer ces tests}

1918	1892	end
1919	1893	end.
1920	1894
1921		Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t).
1922		Proof.
1923		simple induction t; simpl;
	1895	Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace).
	1896	Proof.
	1897	simple induction trace; simpl;
1924	1898	[ exact reduce_stable
1925	1899	\| intros stp l H; case stp;
1926	1900	[ apply compose_term_stable;

2092	2066	Theorem constant_not_nul_valid :
2093	2067	forall i : nat, valid_hyps (constant_not_nul i).
2094	2068	Proof.
2095		unfold valid_hyps, constant_not_nul; intros;
2096		generalize (nth_valid ep e i lp); Simplify; simpl.
2097
2098		elim_beq i1 i0; auto; simpl; intros H1 H2;
2099		elim H1; symmetry ; auto.
	2069	unfold valid_hyps, constant_not_nul; intros i ep e lp H.
	2070	generalize (nth_valid ep e i lp H); Simplify.
2100	2071	Qed.
2101	2072
2102	2073	(* \paragraph{[O_CONSTANT_NEG]} *)

2130	2101	end.
2131	2102
2132	2103	Theorem not_exact_divide_valid :
2133		forall (k1 k2 : int) (body : term) (t i : nat),
2134		valid_hyps (not_exact_divide k1 k2 body t i).
	2104	forall (k1 k2 : int) (body : term) (t0 i : nat),
	2105	valid_hyps (not_exact_divide k1 k2 body t0 i).
2135	2106	Proof.
2136	2107	unfold valid_hyps, not_exact_divide; intros;
2137	2108	generalize (nth_valid ep e i lp); Simplify.
2138		rewrite (scalar_norm_add_stable t e), <-H1.
	2109	rewrite (scalar_norm_add_stable t0 e), <-H1.
2139	2110	do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros.
2140	2111	absurd (interp_term e body * k1 + k2 = 0);
2141	2112	[ now apply OMEGA4 \| symmetry; auto ].

2508	2479	execute_omega cont (apply_oper_2 i1 i2 (state m s) l)
2509	2480	end.
2510	2481
2511		Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t).
2512		Proof.
2513		simple induction t; simpl;
	2482	Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
	2483	Proof.
	2484	simple induction tr; simpl;
2514	2485	[ unfold valid_list_hyps; simpl; intros; left;
2515	2486	apply (constant_not_nul_valid n ep e lp H)
2516	2487	\| unfold valid_list_hyps; simpl; intros; left;

2521	2492	(apply_oper_1_valid m (divide_and_approx k1 k2 body n)
2522	2493	(divide_and_approx_valid k1 k2 body n) ep e lp H)
2523	2494	\| unfold valid_list_hyps; simpl; intros; left;
2524		apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H)
	2495	apply (not_exact_divide_valid _ _ _ _ _ ep e lp H)
2525	2496	\| unfold valid_list_hyps, valid_hyps;
2526	2497	intros k body n t' Ht' m ep e lp H; apply Ht';
2527	2498	apply

2617	2588	(* \subsubsection{Exécution de la trace} *)
2618	2589
2619	2590	Theorem execute_goal :
2620		forall (t : t_omega) (ep : list Prop) (env : list int) (l : hyps),
2621		interp_list_goal ep env (execute_omega t l) -> interp_goal ep env l.
2622		Proof.
2623		intros; apply (goal_valid (execute_omega t) (omega_valid t) ep env l H).
	2591	forall (tr : t_omega) (ep : list Prop) (env : list int) (l : hyps),
	2592	interp_list_goal ep env (execute_omega tr l) -> interp_goal ep env l.
	2593	Proof.
	2594	intros; apply (goal_valid (execute_omega tr) (omega_valid tr) ep env l H).
2624	2595	Qed.
2625	2596
2626	2597

2935	2906	\| intro; apply ne_left_2; assumption ]
2936	2907	\| case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s);
2937	2908	simpl; intro H1;
2938		[ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1;
	2909	[ rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1;
2939	2910	rewrite plus_permute; rewrite plus_opp_r;
2940	2911	rewrite plus_0_r; trivial
2941		\| apply (fun a b => plus_le_reg_r a b (- interp_term e t));
	2912	\| apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
2942	2913	rewrite plus_opp_r; assumption
2943	2914	\| rewrite ge_le_iff;
2944		apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
	2915	apply (fun a b => plus_le_reg_r a b (- interp_term e t1));
2945	2916	rewrite plus_opp_r; assumption
2946	2917	\| rewrite gt_lt_iff; apply lt_left_inv; assumption
2947	2918	\| apply lt_left_inv; assumption

+1

-0

plugins/subtac/subtac_obligations.ml less more

662	662	let admit_obligations n =
663	663	let prg = get_prog_err n in
664	664	let obls, rem = prg.prg_obligations in
	665	let obls = Array.copy obls in
665	666	Array.iteri
666	667	(fun i x ->
667	668	match x.obl_body with

+1

-1

pretyping/cases.ml less more

1762	1762	(* First strategy: we build an "inversion" predicate *)
1763	1763	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
1764	1764	(* Second strategy: we directly use the evar as a non dependent pred *)
1765		let pred2 = lift (List.length arsign) t in
	1765	let pred2 = lift (List.length (List.flatten arsign)) t in
1766	1766	[sigma1, pred1; sigma, pred2]
1767	1767	(* Some type annotation *)
1768	1768	\| Some rtntyp, _ ->

+2

-0

pretyping/detyping.ml less more

388	388	with _ ->
389	389	GVar (dl, id))
390	390	\| Sort s -> GSort (dl,detype_sort s)
	391	\| Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
	392	detype isgoal avoid env c1
391	393	\| Cast (c1,k,c2) ->
392	394	GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2))
393	395	\| Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c

+26

-16

pretyping/evarutil.ml less more

134	134
135	135	let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
136	136
137		let noccur_evar evd evk c =
138		let rec occur_rec c = match kind_of_term c with
139		\| Evar (evk',_ as ev') ->
	137	let noccur_evar env evd evk c =
	138	let rec occur_rec k c = match kind_of_term c with
	139	\| Evar (evk',args' as ev') ->
140	140	(match safe_evar_value evd ev' with
141		\| Some c -> occur_rec c
142		\| None -> if evk = evk' then raise Occur)
143		\| _ -> iter_constr occur_rec c
	141	\| Some c -> occur_rec k c
	142	\| None ->
	143	if evk = evk' then raise Occur else Array.iter (occur_rec k) args')
	144	\| Rel i when i > k ->
	145	(match pi2 (Environ.lookup_rel (i-k) env) with
	146	\| None -> ()
	147	\| Some b -> occur_rec k (lift i b))
	148	\| _ -> iter_constr_with_binders succ occur_rec k c
144	149	in
145		try occur_rec c; true with Occur -> false
	150	try occur_rec 0 c; true with Occur -> false
146	151
147	152	let normalize_evar evd ev =
148	153	match kind_of_term (whd_evar evd (mkEvar ev)) with

740	745	None
741	746
742	747	let is_unification_pattern_evar env evd (evk,args) l t =
743		if List.for_all (fun x -> isRel x \|\| isVar x) l & noccur_evar evd evk t then
	748	if List.for_all (fun x -> isRel x \|\| isVar x) l & noccur_evar env evd evk t
	749	then
744	750	let args = remove_instance_local_defs evd evk (Array.to_list args) in
745	751	let n = List.length args in
746	752	match find_unification_pattern_args env (args @ l) t with

1111	1117	\| Not_found -> CannotInvert
1112	1118	\| NotUnique -> Invertible NoUniqueProjection
1113	1119
1114		let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
	1120	let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
1115	1121	let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
1116	1122	match res with
1117		\| Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) ->
	1123	\| Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
	1124	->
1118	1125	CannotInvert
1119	1126	\| _ ->
1120	1127	res

1152	1159
1153	1160	let filter_of_projection = function Invertible _ -> true \| _ -> false
1154	1161
1155		let invert_invertible_arg evd aliases k (evk,argsv) args' =
	1162	let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
1156	1163	let evi = Evd.find_undefined evd evk in
1157	1164	let subst,_ = make_projectable_subst aliases evd evi argsv in
1158		let projs = array_map_to_list (invert_arg evd aliases k evk subst) args' in
	1165	let projs =
	1166	array_map_to_list (invert_arg fullenv evd aliases k evk subst) args' in
1159	1167	Array.of_list (extract_unique_projections projs)
1160	1168
1161	1169	(* Redefines an evar with a smaller context (i.e. it may depend on less

1363	1371
1364	1372	let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
1365	1373	let filter1 =
1366		restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1)
	1374	restrict_upon_filter evd evk1 (noccur_evar env evd evk2)
	1375	(Array.to_list argsv1)
1367	1376	in
1368	1377	let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
1369	1378	let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
1370	1379	let filter2 =
1371		restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2)
	1380	restrict_upon_filter evd evk2 (noccur_evar env evd evk1)
	1381	(Array.to_list argsv2)
1372	1382	in
1373	1383	let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
1374	1384	let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in

1388	1398	try
1389	1399	let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
1390	1400	let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
1391		evd,mkEvar (evk1',invert_invertible_arg evd aliases k2 ev2 args1)
	1401	evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1)
1392	1402	with
1393	1403	\| EvarSolvedWhileRestricting (evd,ev1) ->
1394	1404	raise (EvarSolvedOnTheFly (evd,ev1))

1584	1594	let aliases = lift_aliases k aliases in
1585	1595	(try
1586	1596	let ev = (evk,Array.map (lift k) argsv) in
1587		let evd,body = project_evar_on_evar conv_algo env !evdref aliases k ev' ev in
	1597	let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev' ev in
1588	1598	evdref := evd;
1589	1599	body
1590	1600	with

+32

-2

pretyping/glob_term.ml less more

345	345	\| GHole (loc,_) -> PatVar (loc,na)
346	346	\| GRef (loc,ConstructRef cstr) ->
347	347	PatCstr (loc,cstr,[],na)
348		\| GApp (loc,GRef (_,ConstructRef cstr),l) ->
349		PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
	348	\| GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
	349	let mib,_ = Global.lookup_inductive ind in
	350	let nparams = mib.Declarations.mind_nparams in
	351	if nparams > List.length args then
	352	user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
	353	let params,args = list_chop nparams args in
	354	List.iter (function GHole _ -> ()
	355	\| _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
	356	params;
	357	let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
	358	PatCstr (loc,cstr,args,na)
	359	\| _ -> raise Not_found
	360
	361	let rec cases_pattern_of_glob_constr na = function
	362	\| GVar (loc,id) when na<>Anonymous ->
	363	(* Unable to manage the presence of both an alias and a variable *)
	364	raise Not_found
	365	\| GVar (loc,id) -> PatVar (loc,Name id)
	366	\| GHole (loc,_) -> PatVar (loc,na)
	367	\| GRef (loc,ConstructRef cstr) ->
	368	PatCstr (loc,cstr,[],na)
	369	\| GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
	370	let mib,_ = Global.lookup_inductive ind in
	371	let nparams = mib.Declarations.mind_nparams in
	372	if nparams > List.length args then
	373	user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
	374	let params,args = list_chop nparams args in
	375	List.iter (function GHole _ -> ()
	376	\| _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
	377	params;
	378	let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
	379	PatCstr (loc,cstr,args,na)
350	380	\| _ -> raise Not_found
351	381
352	382	(* Turn a closed cases pattern into a glob_constr *)

+7

-2

pretyping/typing.ml less more

40	40	let (evd,s) = Evarutil.define_evar_as_sort !evdref ev in
41	41	evdref := evd; { utj_val = j.uj_val; utj_type = s }
42	42	\| _ -> error_not_type env j
	43
	44	let e_assumption_of_judgment env evdref j =
	45	try (e_type_judgment env evdref j).utj_val
	46	with TypeError _ ->
	47	error_assumption env j
43	48
44	49	let e_judge_of_apply env evdref funj argjv =
45	50	let rec apply_rec n typ = function

149	154	\| Evar ev ->
150	155	let ty = Evd.existential_type !evdref ev in
151	156	let jty = execute env evdref (whd_evar !evdref ty) in
152		let jty = assumption_of_judgment env jty in
	157	let jty = e_assumption_of_judgment env evdref jty in
153	158	{ uj_val = cstr; uj_type = jty }
154	159
155	160	\| Rel n ->

242	247
243	248	and execute_recdef env evdref (names,lar,vdef) =
244	249	let larj = execute_array env evdref lar in
245		let lara = Array.map (assumption_of_judgment env) larj in
	250	let lara = Array.map (e_assumption_of_judgment env evdref) larj in
246	251	let env1 = push_rec_types (names,lara,vdef) env in
247	252	let vdefj = execute_array env1 evdref vdef in
248	253	let vdefv = Array.map j_val vdefj in

+21

-35

pretyping/unification.ml less more

197	197	(* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *)
198	198
199	199	modulo_delta : Names.transparent_state;
200		(* This controls which constant are unfoldable; this is on for apply *)
	200	(* This controls which constants are unfoldable; this is on for apply *)
201	201	(* (but not simple apply) since Feb 2008 for 8.2 *)
202	202
203	203	modulo_delta_types : Names.transparent_state;
	204
	205	modulo_delta_in_merge : Names.transparent_state option;
	206	(* This controls whether unfoldability is different when trying to unify *)
	207	(* several instances of the same metavariable *)
	208	(* Typical situation is when we give a pattern to be matched *)
	209	(* syntactically against a subterm but we want the metas of the *)
	210	(* pattern to be modulo convertibility *)
204	211
205	212	check_applied_meta_types : bool;
206	213	(* This controls whether meta's applied to arguments have their *)

239	246	}
240	247
241	248	(* Default flag for unifying a type against a type (e.g. apply) *)
242		(* We set all conversion flags *)
	249	(* We set all conversion flags (no flag should be modified anymore) *)
243	250	let default_unify_flags = {
244	251	modulo_conv_on_closed_terms = Some full_transparent_state;
245	252	use_metas_eagerly_in_conv_on_closed_terms = true;
246	253	modulo_delta = full_transparent_state;
247	254	modulo_delta_types = full_transparent_state;
	255	modulo_delta_in_merge = None;
248	256	check_applied_meta_types = true;
249	257	resolve_evars = false;
250	258	use_pattern_unification = true;

257	265	(* in fact useless when not used in w_unify_to_subterm_list *)
258	266	}
259	267
	268	let set_merge_flags flags =
	269	match flags.modulo_delta_in_merge with
	270	\| None -> flags
	271	\| Some ts ->
	272	{ flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts }
	273
260	274	(* Default flag for the "simple apply" version of unification of a *)
261	275	(* type against a type (e.g. apply) *)
262	276	(* We set only the flags available at the time the new "apply" extends *)
263	277	(* out of "simple apply" *)
264		let default_no_delta_unify_flags = {
265		modulo_conv_on_closed_terms = Some full_transparent_state;
266		use_metas_eagerly_in_conv_on_closed_terms = true;
	278	let default_no_delta_unify_flags = { default_unify_flags with
267	279	modulo_delta = empty_transparent_state;
268		modulo_delta_types = full_transparent_state;
269	280	check_applied_meta_types = false;
270		resolve_evars = false;
271	281	use_pattern_unification = false;
272	282	use_meta_bound_pattern_unification = true;
273		frozen_evars = ExistentialSet.empty;
274		restrict_conv_on_strict_subterms = false;
275	283	modulo_betaiota = false;
276		modulo_eta = true;
277		allow_K_in_toplevel_higher_order_unification = false
278	284	}
279	285
280	286	(* Default flags for looking for subterms in elimination tactics *)

282	288	(* allow_K) because only closed terms are involved in *)
283	289	(* induction/destruct/case/elim and w_unify_to_subterm_list does not *)
284	290	(* call w_unify for induction/destruct/case/elim (13/6/2011) *)
285		let elim_flags = {
286		modulo_conv_on_closed_terms = Some full_transparent_state;
287		use_metas_eagerly_in_conv_on_closed_terms = true;
288		modulo_delta = full_transparent_state;
289		modulo_delta_types = full_transparent_state;
290		check_applied_meta_types = true;
291		resolve_evars = false;
292		use_pattern_unification = true;
293		use_meta_bound_pattern_unification = true;
294		frozen_evars = ExistentialSet.empty;
	291	let elim_flags = { default_unify_flags with
295	292	restrict_conv_on_strict_subterms = false; (* ? *)
296	293	modulo_betaiota = false;
297		modulo_eta = true;
298	294	allow_K_in_toplevel_higher_order_unification = true
299	295	}
300	296
301		let elim_no_delta_flags = {
302		modulo_conv_on_closed_terms = Some full_transparent_state;
303		use_metas_eagerly_in_conv_on_closed_terms = true;
	297	let elim_no_delta_flags = { elim_flags with
304	298	modulo_delta = empty_transparent_state;
305		modulo_delta_types = full_transparent_state;
306	299	check_applied_meta_types = false;
307		resolve_evars = false;
308	300	use_pattern_unification = false;
309		use_meta_bound_pattern_unification = true;
310		frozen_evars = ExistentialSet.empty;
311		restrict_conv_on_strict_subterms = false; (* ? *)
312		modulo_betaiota = false;
313		modulo_eta = true;
314		allow_K_in_toplevel_higher_order_unification = true
315	301	}
316	302
317	303	let set_no_head_reduction flags =

864	850	if Evd.is_defined evd evk then
865	851	let v = Evd.existential_value evd ev in
866	852	let (evd,metas',evars'') =
867		unify_0 curenv evd CONV flags rhs v in
	853	unify_0 curenv evd CONV (set_merge_flags flags) rhs v in
868	854	w_merge_rec evd (metas'@metas) (evars''@evars') eqns
869	855	else begin
870	856	(* This can make rhs' ill-typed if metas are *)

942	928	let sp_env = Global.env_of_context ev.evar_hyps in
943	929	let (evd', c) = applyHead sp_env evd nargs hdc in
944	930	let (evd'',mc,ec) =
945		unify_0 sp_env evd' CUMUL flags
	931	unify_0 sp_env evd' CUMUL (set_merge_flags flags)
946	932	(get_type_of sp_env evd' c) ev.evar_concl in
947	933	let evd''' = w_merge_rec evd'' mc ec [] in
948	934	if evd' == evd'''

+1

-0

pretyping/unification.mli less more

14	14	use_metas_eagerly_in_conv_on_closed_terms : bool;
15	15	modulo_delta : Names.transparent_state;
16	16	modulo_delta_types : Names.transparent_state;
	17	modulo_delta_in_merge : Names.transparent_state option;
17	18	check_applied_meta_types : bool;
18	19	resolve_evars : bool;
19	20	use_pattern_unification : bool;

+1

-0

proofs/clenvtac.ml less more

104	104	use_metas_eagerly_in_conv_on_closed_terms = false;
105	105	modulo_delta = empty_transparent_state;
106	106	modulo_delta_types = full_transparent_state;
	107	modulo_delta_in_merge = None;
107	108	check_applied_meta_types = false;
108	109	resolve_evars = false;
109	110	use_pattern_unification = false;

+5

-2

proofs/pfedit.ml less more

61	61
62	62	let start_proof id str hyps c ?init_tac ?compute_guard hook =
63	63	let goals = [ (Global.env_of_context hyps , c) ] in
64		let init_tac = Option.map Proofview.V82.tactic init_tac in
65	64	Proof_global.start_proof id str goals ?compute_guard hook;
66		try Option.iter Proof_global.run_tactic init_tac
	65	let tac = match init_tac with
	66	\| Some tac -> Proofview.V82.tactic tac
	67	\| None -> Proofview.tclUNIT ()
	68	in
	69	try Proof_global.run_tactic tac
67	70	with e -> Proof_global.discard_current (); raise e
68	71
69	72	let restart_proof () = undo_todepth 1

+13

-12

scripts/coqmktop.ml less more

62	62
63	63	let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
64	64
	65	(* Since the .cma are given with their relative paths (e.g. "lib/clib.cma"),
	66	we only need to include directories mentionned in the temp main ml file
	67	below (for accessing the corresponding .cmi). *)
	68
65	69	let src_dirs =
66		[ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ]
	70	[ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]; ]
67	71
68	72	let includes () =
69		(if !Flags.boot then [] (* the include flags are given on the cmdline *)
70		else
71		let coqlib = Envars.coqlib () in
72		let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
73		let camlp4incl = ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""] in
74		List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs camlp4incl)
	73	let coqlib = if !Flags.boot then "." else Envars.coqlib () in
	74	let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
	75	(List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
	76	@ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
75	77	@ (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
76	78
77	79	(* Transform bytecode object file names in native object file names *)

241	243
242	244	(* create a temporary main file to link *)
243	245	let create_tmp_main_file modules =
244		let main_name = Filename.temp_file "coqmain" ".ml" in
245		let oc = open_out main_name in
	246	let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
246	247	try
247	248	(* Add the pre-linked modules *)
248	249	output_string oc "List.iter Mltop.add_known_module [\"";

289	290	[]
290	291	in
291	292	(* the list of the loaded modules *)
292		let main_file = Filename.quote (create_tmp_main_file modules) in
	293	let main_file = create_tmp_main_file modules in
293	294	try
294		let args =
295		options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in
	295	let args = options @ includes () @ copts @ tolink @ dynlink in
	296	let args = args @ [ Filename.quote main_file ] in
296	297	(* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
297	298	let args = if !top then args @ [ "topstart.cmo" ] else args in
298	299	(* Now, with the .cma, we MUST use the -linkall option *)

+1

-0

tactics/auto.ml less more

1019	1019	use_metas_eagerly_in_conv_on_closed_terms = false;
1020	1020	modulo_delta = empty_transparent_state;
1021	1021	modulo_delta_types = full_transparent_state;
	1022	modulo_delta_in_merge = None;
1022	1023	check_applied_meta_types = false;
1023	1024	resolve_evars = true;
1024	1025	use_pattern_unification = false;

+1

-0

tactics/class_tactics.ml4 less more

76	76	use_metas_eagerly_in_conv_on_closed_terms = true;
77	77	modulo_delta = var_full_transparent_state;
78	78	modulo_delta_types = full_transparent_state;
	79	modulo_delta_in_merge = None;
79	80	check_applied_meta_types = false;
80	81	resolve_evars = false;
81	82	use_pattern_unification = true;

+2

-0

tactics/equality.ml less more

86	86	Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
87	87	Unification.modulo_delta = empty_transparent_state;
88	88	Unification.modulo_delta_types = empty_transparent_state;
	89	Unification.modulo_delta_in_merge = None;
89	90	Unification.check_applied_meta_types = true;
90	91	Unification.resolve_evars = true;
91	92	Unification.use_pattern_unification = true;

154	155
155	156	Unification.modulo_delta = empty_transparent_state;
156	157	Unification.modulo_delta_types = full_transparent_state;
	158	Unification.modulo_delta_in_merge = None;
157	159	Unification.check_applied_meta_types = true;
158	160	Unification.resolve_evars = false;
159	161	Unification.use_pattern_unification = true;

+1

-1

tactics/extraargs.ml4 less more

193	193	\| None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "\|-"
194	194	\| Some l,_ ->
195	195	str "in" ++
196		Util.prlist (fun id -> spc () ++ pr_id id) l ++
	196	spc () ++ Util.prlist_with_sep Util.pr_comma pr_id l ++
197	197	match concl with
198	198	\| true -> spc () ++ str "\|-" ++ spc () ++ str "*"
199	199	\| _ -> mt ()

+3

-2

tactics/hipattern.ml4 less more

150	150	\| Ind ind ->
151	151	let car = mis_constr_nargs ind in
152	152	let (mib,mip) = Global.lookup_inductive ind in
153		if array_for_all (fun ar -> ar = 1) car &&
154		not (mis_is_recursive (ind,mib,mip))
	153	if array_for_all (fun ar -> ar = 1) car
	154	&& not (mis_is_recursive (ind,mib,mip))
	155	&& (mip.mind_nrealargs = 0)
155	156	then
156	157	if strict then
157	158	if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then

+4

-1

tactics/rewrite.ml4 less more

293	293	Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
294	294	Unification.modulo_delta = empty_transparent_state;
295	295	Unification.modulo_delta_types = full_transparent_state;
	296	Unification.modulo_delta_in_merge = None;
296	297	Unification.check_applied_meta_types = true;
297	298	Unification.resolve_evars = true;
298	299	Unification.use_pattern_unification = true;

304	305	Unification.allow_K_in_toplevel_higher_order_unification = true
305	306	}
306	307
307		let rewrite2_unif_flags =
	308	let rewrite2_unif_flags =
308	309	{ Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
309	310	Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
310	311	Unification.modulo_delta = empty_transparent_state;
311	312	Unification.modulo_delta_types = conv_transparent_state;
	313	Unification.modulo_delta_in_merge = None;
312	314	Unification.check_applied_meta_types = true;
313	315	Unification.resolve_evars = true;
314	316	Unification.use_pattern_unification = true;

326	328	Unification.use_metas_eagerly_in_conv_on_closed_terms = true;
327	329	Unification.modulo_delta = ts;
328	330	Unification.modulo_delta_types = ts;
	331	Unification.modulo_delta_in_merge = None;
329	332	Unification.check_applied_meta_types = true;
330	333	Unification.resolve_evars = true;
331	334	Unification.use_pattern_unification = true;

+1

-0

tactics/tactics.ml less more

1689	1689	use_metas_eagerly_in_conv_on_closed_terms = false;
1690	1690	modulo_delta = empty_transparent_state;
1691	1691	modulo_delta_types = full_transparent_state;
	1692	modulo_delta_in_merge = Some full_transparent_state;
1692	1693	check_applied_meta_types = true;
1693	1694	resolve_evars = false;
1694	1695	use_pattern_unification = false;

+9

-0

test-suite/output/Notations.out less more

126	126	: nat
127	127	fun _ : nat => 9
128	128	: nat -> nat
	129	Identifier 'ONE' now a keyword
	130	fun (x : nat) (p : x = x) => match p with
	131	\| ONE => ONE
	132	end = p
	133	: forall x : nat, x = x -> Prop
	134	fun (x : nat) (p : x = x) => match p with
	135	\| 1 => 1
	136	end = p
	137	: forall x : nat, x = x -> Prop

+13

-0

test-suite/output/Notations.v less more

261	261
262	262	Check (foo 9).
263	263	Check (fun _ : nat => 9).
	264
	265	(* Checking parsing and printing of numerical and non-numerical notations for eq_refl *)
	266
	267	(* This notation was not correctly printed until Pierre B.'s
	268	improvements to the interpretation of patterns *)
	269
	270	Notation "'ONE'" := eq_refl.
	271	Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p.
	272
	273	(* This one used to failed at parsing until now *)
	274
	275	Notation "1" := eq_refl.
	276	Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p.

+6

-0

test-suite/success/Cases.v less more

1864	1864	\| Z0 => true
1865	1865	\| _ => false
1866	1866	end).
	1867
	1868	(* Check that types with unknown sort, as A below, are not fatal to
	1869	the pattern-matching compilation *)
	1870
	1871	Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
	1872	match p with eq_refl => u end.

+13

-2

test-suite/success/set.v less more

	0	(* This used to fail in 8.0pl1 *)
	1
0	2	Goal forall n, n+n=0->0=n+n.
1	3	intros.
	4	set n in * \|-.
	5	Abort.
2	6
3		(* This used to fail in 8.0pl1 *)
4		set n in * \|-.
	7	(* This works from 8.4pl1, since merging of different instances of the
	8	same metavariable in a pattern is done modulo conversion *)
	9
	10	Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1").
	11
	12	Goal forall (f:forall n, n=0 -> Prop) n (H:(n+n).+1=0), f (n.+1+n) H.
	13	intros.
	14	set (f _ _).
	15	Abort.
5	16
6	17
7	18

+1

-0

theories/FSets/FMapAVL.v less more

34	34	Local Open Scope pair_scope.
35	35	Local Open Scope lazy_bool_scope.
36	36	Local Open Scope Int_scope.
	37	Local Notation int := I.t.
37	38
38	39	Definition key := X.t.
39	40	Hint Transparent key.

+1

-0

theories/MSets/MSetAVL.v less more

43	43
44	44	Module Ops (Import I:Int)(X:OrderedType) <: MSetInterface.Ops X.
45	45	Local Open Scope Int_scope.
	46	Local Notation int := I.t.
46	47
47	48	( Generic trees instantiated with integer height *)
48	49

+3

-7

theories/Numbers/NatInt/NZOrder.v less more

146	146	Definition le_lteq := lt_eq_cases.
147	147
148	148	Module Private_OrderTac.
149		Module Elts <: TotalOrder.
150		Definition t := t.
151		Definition eq := eq.
152		Definition lt := lt.
153		Definition le := le.
	149	Module IsTotal.
154	150	Definition eq_equiv := eq_equiv.
155	151	Definition lt_strorder := lt_strorder.
156	152	Definition lt_compat := lt_compat.
157	153	Definition lt_total := lt_total.
158	154	Definition le_lteq := le_lteq.
159		End Elts.
160		Module Tac := !MakeOrderTac Elts.
	155	End IsTotal.
	156	Module Tac := !MakeOrderTac NZ IsTotal.
161	157	End Private_OrderTac.
162	158	Ltac order := Private_OrderTac.Tac.order.
163	159

+2

-2

theories/Numbers/Rational/BigQ/BigQ.v less more

41	41	Bind Scope bigQ_scope with t t_.
42	42	Include !QProperties <+ HasEqBool2Dec
43	43	<+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
	44	Ltac order := Private_Tac.order.
44	45	End BigQ.
45	46
46	47	(** Notations about [BigQ] *)

143	144
144	145	(** [BigQ] can also benefit from an "order" tactic *)
145	146
146		Module BigQ_Order := !OrdersTac.MakeOrderTac BigQ.
147		Ltac bigQ_order := BigQ_Order.order.
	147	Ltac bigQ_order := BigQ.order.
148	148
149	149	Section TestOrder.
150	150	Let test : forall x y : bigQ, x<=y -> y<=x -> x==y.

+2

-0

theories/PArith/BinPos.v less more

1484	1484	(** We hence obtain all the generic properties of [min] and [max]. *)
1485	1485
1486	1486	Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
	1487
	1488	Ltac order := Private_Tac.order.
1487	1489
1488	1490	(** Minimum, maximum and constant one *)
1489	1491

+257

-266

theories/Structures/GenericMinMax.v less more

39	39	Definition max := gmax O.compare.
40	40	Definition min := gmin O.compare.
41	41
42		Lemma ge_not_lt : forall x y, y<=x -> x<y -> False.
	42	Lemma ge_not_lt x y : y<=x -> x<y -> False.
43	43	Proof.
44		intros x y H H'.
	44	intros H H'.
45	45	apply (StrictOrder_Irreflexive x).
46	46	rewrite le_lteq in *; destruct H as [H\|H].
47	47	transitivity y; auto.
48	48	rewrite H in H'; auto.
49	49	Qed.
50	50
51		Lemma max_l : forall x y, y<=x -> max x y == x.
	51	Lemma max_l x y : y<=x -> max x y == x.
52	52	Proof.
53	53	intros. unfold max, gmax. case compare_spec; auto with relations.
54	54	intros; elim (ge_not_lt x y); auto.
55	55	Qed.
56	56
57		Lemma max_r : forall x y, x<=y -> max x y == y.
	57	Lemma max_r x y : x<=y -> max x y == y.
58	58	Proof.
59	59	intros. unfold max, gmax. case compare_spec; auto with relations.
60	60	intros; elim (ge_not_lt y x); auto.
61	61	Qed.
62	62
63		Lemma min_l : forall x y, x<=y -> min x y == x.
	63	Lemma min_l x y : x<=y -> min x y == x.
64	64	Proof.
65	65	intros. unfold min, gmin. case compare_spec; auto with relations.
66	66	intros; elim (ge_not_lt y x); auto.
67	67	Qed.
68	68
69		Lemma min_r : forall x y, y<=x -> min x y == y.
	69	Lemma min_r x y : y<=x -> min x y == y.
70	70	Proof.
71	71	intros. unfold min, gmin. case compare_spec; auto with relations.
72	72	intros; elim (ge_not_lt x y); auto.

75	75	End GenericMinMax.
76	76
77	77
78		( Consequences of the minimalist interface: facts about [max]. *)
79
80		Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
81		Module Import Private_Tac := !MakeOrderTac O.
	78	( Consequences of the minimalist interface: facts about [max] and [min]. *)
	79
	80	Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
	81	Module Import Private_Tac := !MakeOrderTac O O.
82	82
83	83	(** An alternative caracterisation of [max], equivalent to
84	84	[max_l /\ max_r] *)
85	85
86		Lemma max_spec : forall n m,
87		(n < m /\ max n m == m) \/ (m <= n /\ max n m == n).
88		Proof.
89		intros n m.
	86	Lemma max_spec n m :
	87	(n < m /\ max n m == m) \/ (m <= n /\ max n m == n).
	88	Proof.
90	89	destruct (lt_total n m); [left\|right].
91		split; auto. apply max_r. rewrite le_lteq; auto.
92		assert (m <= n) by (rewrite le_lteq; intuition).
93		split; auto. apply max_l; auto.
	90	- split; auto. apply max_r. rewrite le_lteq; auto.
	91	- assert (m <= n) by (rewrite le_lteq; intuition).
	92	split; auto. now apply max_l.
94	93	Qed.
95	94
96	95	(** A more symmetric version of [max_spec], based only on [le].
97	96	Beware that left and right alternatives overlap. *)
98	97
99		Lemma max_spec_le : forall n m,
	98	Lemma max_spec_le n m :
100	99	(n <= m /\ max n m == m) \/ (m <= n /\ max n m == n).
101	100	Proof.
102		intros. destruct (max_spec n m); [left\|right]; intuition; order.
	101	destruct (max_spec n m); [left\|right]; intuition; order.
103	102	Qed.
104	103
105	104	Instance : Proper (eq==>eq==>iff) le.

107	106
108	107	Instance max_compat : Proper (eq==>eq==>eq) max.
109	108	Proof.
110		intros x x' Hx y y' Hy.
111		assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
112		set (m := max x y) in ; set (m' := max x' y') in ; clearbody m m'.
113		rewrite <- Hx, <- Hy in *.
114		destruct (lt_total x y); intuition order.
115		Qed.
116
	109	intros x x' Hx y y' Hy.
	110	assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
	111	set (m := max x y) in ; set (m' := max x' y') in ; clearbody m m'.
	112	rewrite <- Hx, <- Hy in *.
	113	destruct (lt_total x y); intuition order.
	114	Qed.
117	115
118	116	(** A function satisfying the same specification is equal to [max]. *)
119	117
120		Lemma max_unicity : forall n m p,
121		((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m.
122		Proof.
123		intros. assert (Hm := max_spec n m).
	118	Lemma max_unicity n m p :
	119	((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m.
	120	Proof.
	121	assert (Hm := max_spec n m).
124	122	destruct (lt_total n m); intuition; order.
125	123	Qed.
126	124
127		Lemma max_unicity_ext : forall f,
128		(forall n m, (n < m /\ f n m == m) \/ (m <= n /\ f n m == n)) ->
	125	Lemma max_unicity_ext f :
	126	(forall n m, (n < m /\ f n m == m) \/ (m <= n /\ f n m == n)) ->
129	127	(forall n m, f n m == max n m).
130	128	Proof.
131	129	intros. apply max_unicity; auto.

133	131
134	132	(** [max] commutes with monotone functions. *)
135	133
136		Lemma max_mono: forall f,
	134	Lemma max_mono f :
137	135	(Proper (eq ==> eq) f) ->
138	136	(Proper (le ==> le) f) ->
139	137	forall x y, max (f x) (f y) == f (max x y).
140	138	Proof.
141		intros f Eqf Lef x y.
	139	intros Eqf Lef x y.
142	140	destruct (max_spec x y) as [(H,E)\|(H,E)]; rewrite E;
143	141	destruct (max_spec (f x) (f y)) as [(H',E')\|(H',E')]; auto.
144	142	assert (f x <= f y) by (apply Lef; order). order.

147	145
148	146	( * Semi-lattice algebraic properties of [max] *)
149	147
150		Lemma max_id : forall n, max n n == n.
151		Proof.
152		intros. destruct (max_spec n n); intuition.
	148	Lemma max_id n : max n n == n.
	149	Proof.
	150	apply max_l; order.
153	151	Qed.
154	152
155	153	Notation max_idempotent := max_id (only parsing).
156	154
157		Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p.
158		Proof.
159		intros.
160		destruct (max_spec n p) as [(H,Eq)\|(H,Eq)]; rewrite Eq.
161		destruct (max_spec m n) as [(H',Eq')\|(H',Eq')]; rewrite Eq'.
162		destruct (max_spec m p); intuition; order. order.
163		destruct (max_spec m n) as [(H',Eq')\|(H',Eq')]; rewrite Eq'. order.
164		destruct (max_spec m p); intuition; order.
165		Qed.
166
167		Lemma max_comm : forall n m, max n m == max m n.
168		Proof.
169		intros.
170		destruct (max_spec n m) as [(H,Eq)\|(H,Eq)]; rewrite Eq.
171		destruct (max_spec m n) as [(H',Eq')\|(H',Eq')]; rewrite Eq'; order.
172		destruct (max_spec m n) as [(H',Eq')\|(H',Eq')]; rewrite Eq'; order.
173		Qed.
	155	Lemma max_assoc m n p : max m (max n p) == max (max m n) p.
	156	Proof.
	157	destruct (max_spec n p) as [(H,E)\|(H,E)]; rewrite E;
	158	destruct (max_spec m n) as [(H',E')\|(H',E')]; rewrite E', ?E; try easy.
	159	- apply max_r; order.
	160	- symmetry. apply max_l; order.
	161	Qed.
	162
	163	Lemma max_comm n m : max n m == max m n.
	164	Proof.
	165	destruct (max_spec m n) as [(H,E)\|(H,E)]; rewrite E;
	166	(apply max_r \|\| apply max_l); order.
	167	Qed.
	168
	169	Ltac solve_max :=
	170	match goal with \|- context [max ?n ?m] =>
	171	destruct (max_spec n m); intuition; order
	172	end.
174	173
175	174	( * Least-upper bound properties of [max] *)
176	175
177		Lemma le_max_l : forall n m, n <= max n m.
178		Proof.
179		intros; destruct (max_spec n m); intuition; order.
180		Qed.
181
182		Lemma le_max_r : forall n m, m <= max n m.
183		Proof.
184		intros; destruct (max_spec n m); intuition; order.
185		Qed.
186
187		Lemma max_l_iff : forall n m, max n m == n <-> m <= n.
188		Proof.
189		split. intro H; rewrite <- H. apply le_max_r. apply max_l.
190		Qed.
191
192		Lemma max_r_iff : forall n m, max n m == m <-> n <= m.
193		Proof.
194		split. intro H; rewrite <- H. apply le_max_l. apply max_r.
195		Qed.
196
197		Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m.
198		Proof.
199		intros n m p H; destruct (max_spec n m);
200		[right\|left]; intuition; order.
201		Qed.
202
203		Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m.
204		Proof.
205		intros. split. apply max_le.
206		destruct (max_spec n m); intuition; order.
207		Qed.
208
209		Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m.
210		Proof.
211		intros. destruct (max_spec n m); intuition;
	176	Lemma le_max_l n m : n <= max n m.
	177	Proof. solve_max. Qed.
	178
	179	Lemma le_max_r n m : m <= max n m.
	180	Proof. solve_max. Qed.
	181
	182	Lemma max_l_iff n m : max n m == n <-> m <= n.
	183	Proof. solve_max. Qed.
	184
	185	Lemma max_r_iff n m : max n m == m <-> n <= m.
	186	Proof. solve_max. Qed.
	187
	188	Lemma max_le n m p : p <= max n m -> p <= n \/ p <= m.
	189	Proof.
	190	destruct (max_spec n m); [right\|left]; intuition; order.
	191	Qed.
	192
	193	Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m.
	194	Proof. split. apply max_le. solve_max. Qed.
	195
	196	Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m.
	197	Proof.
	198	destruct (max_spec n m); intuition;
212	199	order \|\| (right; order) \|\| (left; order).
213	200	Qed.
214	201
215		Lemma max_lub_l : forall n m p, max n m <= p -> n <= p.
216		Proof.
217		intros; destruct (max_spec n m); intuition; order.
218		Qed.
219
220		Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
221		Proof.
222		intros; destruct (max_spec n m); intuition; order.
223		Qed.
224
225		Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p.
226		Proof.
227		intros; destruct (max_spec n m); intuition; order.
228		Qed.
229
230		Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p.
231		Proof.
232		intros; destruct (max_spec n m); intuition; order.
233		Qed.
234
235		Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p.
236		Proof.
237		intros; destruct (max_spec n m); intuition; order.
238		Qed.
239
240		Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p.
241		Proof.
242		intros; destruct (max_spec n m); intuition; order.
243		Qed.
244
245		Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m.
246		Proof.
247		intros.
248		destruct (max_spec p n) as [(LT,E)\|(LE,E)]; rewrite E.
249		assert (LE' := le_max_r p m). order.
250		apply le_max_l.
251		Qed.
252
253		Lemma max_le_compat_r : forall n m p, n <= m -> max n p <= max m p.
254		Proof.
255		intros. rewrite (max_comm n p), (max_comm m p).
256		auto using max_le_compat_l.
257		Qed.
258
259		Lemma max_le_compat : forall n m p q, n <= m -> p <= q ->
260		max n p <= max m q.
261		Proof.
262		intros n m p q Hnm Hpq.
	202	Lemma max_lub_l n m p : max n m <= p -> n <= p.
	203	Proof. solve_max. Qed.
	204
	205	Lemma max_lub_r n m p : max n m <= p -> m <= p.
	206	Proof. solve_max. Qed.
	207
	208	Lemma max_lub n m p : n <= p -> m <= p -> max n m <= p.
	209	Proof. solve_max. Qed.
	210
	211	Lemma max_lub_iff n m p : max n m <= p <-> n <= p /\ m <= p.
	212	Proof. solve_max. Qed.
	213
	214	Lemma max_lub_lt n m p : n < p -> m < p -> max n m < p.
	215	Proof. solve_max. Qed.
	216
	217	Lemma max_lub_lt_iff n m p : max n m < p <-> n < p /\ m < p.
	218	Proof. solve_max. Qed.
	219
	220	Lemma max_le_compat_l n m p : n <= m -> max p n <= max p m.
	221	Proof. intros. apply max_lub_iff. solve_max. Qed.
	222
	223	Lemma max_le_compat_r n m p : n <= m -> max n p <= max m p.
	224	Proof. intros. apply max_lub_iff. solve_max. Qed.
	225
	226	Lemma max_le_compat n m p q : n <= m -> p <= q -> max n p <= max m q.
	227	Proof.
	228	intros Hnm Hpq.
263	229	assert (LE := max_le_compat_l _ _ m Hpq).
264	230	assert (LE' := max_le_compat_r _ _ p Hnm).
265	231	order.
266	232	Qed.
267	233
268		End MaxLogicalProperties.
269
270
271		( Properties concernant [min], then both [min] and [max].
272
273		To avoid too much code duplication, we exploit that [min] can be
274		seen as a [max] of the reversed order.
275		*)
276
277		Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
278		Include MaxLogicalProperties O M.
279		Import Private_Tac.
280
281		Module Import Private_Rev.
282		Module ORev := TotalOrderRev O.
283		Module MRev <: HasMax ORev.
284		Definition max x y := M.min y x.
285		Definition max_l x y := M.min_r y x.
286		Definition max_r x y := M.min_l y x.
287		End MRev.
288		Module MPRev := MaxLogicalProperties ORev MRev.
289		End Private_Rev.
	234	(** Properties of [min] *)
	235
	236	Lemma min_spec n m :
	237	(n < m /\ min n m == n) \/ (m <= n /\ min n m == m).
	238	Proof.
	239	destruct (lt_total n m); [left\|right].
	240	- split; auto. apply min_l. rewrite le_lteq; auto.
	241	- assert (m <= n) by (rewrite le_lteq; intuition).
	242	split; auto. now apply min_r.
	243	Qed.
	244
	245	Lemma min_spec_le n m :
	246	(n <= m /\ min n m == n) \/ (m <= n /\ min n m == m).
	247	Proof.
	248	destruct (min_spec n m); [left\|right]; intuition; order.
	249	Qed.
290	250
291	251	Instance min_compat : Proper (eq==>eq==>eq) min.
292		Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed.
293
294		Lemma min_spec : forall n m,
295		(n < m /\ min n m == n) \/ (m <= n /\ min n m == m).
296		Proof. intros. exact (MPRev.max_spec m n). Qed.
297
298		Lemma min_spec_le : forall n m,
299		(n <= m /\ min n m == n) \/ (m <= n /\ min n m == m).
300		Proof. intros. exact (MPRev.max_spec_le m n). Qed.
301
302		Lemma min_mono: forall f,
	252	Proof.
	253	intros x x' Hx y y' Hy.
	254	assert (H1 := min_spec x y). assert (H2 := min_spec x' y').
	255	set (m := min x y) in ; set (m' := min x' y') in ; clearbody m m'.
	256	rewrite <- Hx, <- Hy in *.
	257	destruct (lt_total x y); intuition order.
	258	Qed.
	259
	260	Lemma min_unicity n m p :
	261	((n < m /\ p == n) \/ (m <= n /\ p == m)) -> p == min n m.
	262	Proof.
	263	assert (Hm := min_spec n m).
	264	destruct (lt_total n m); intuition; order.
	265	Qed.
	266
	267	Lemma min_unicity_ext f :
	268	(forall n m, (n < m /\ f n m == n) \/ (m <= n /\ f n m == m)) ->
	269	(forall n m, f n m == min n m).
	270	Proof.
	271	intros. apply min_unicity; auto.
	272	Qed.
	273
	274	Lemma min_mono f :
303	275	(Proper (eq ==> eq) f) ->
304	276	(Proper (le ==> le) f) ->
305	277	forall x y, min (f x) (f y) == f (min x y).
306	278	Proof.
307		intros. apply MPRev.max_mono; auto. compute in *; eauto.
308		Qed.
309
310		Lemma min_unicity : forall n m p,
311		((n < m /\ p == n) \/ (m <= n /\ p == m)) -> p == min n m.
312		Proof. intros n m p. apply MPRev.max_unicity. Qed.
313
314		Lemma min_unicity_ext : forall f,
315		(forall n m, (n < m /\ f n m == n) \/ (m <= n /\ f n m == m)) ->
316		(forall n m, f n m == min n m).
317		Proof. intros f H n m. apply MPRev.max_unicity, H; auto. Qed.
318
319		Lemma min_id : forall n, min n n == n.
320		Proof. intros. exact (MPRev.max_id n). Qed.
	279	intros Eqf Lef x y.
	280	destruct (min_spec x y) as [(H,E)\|(H,E)]; rewrite E;
	281	destruct (min_spec (f x) (f y)) as [(H',E')\|(H',E')]; auto.
	282	assert (f x <= f y) by (apply Lef; order). order.
	283	assert (f y <= f x) by (apply Lef; order). order.
	284	Qed.
	285
	286	Lemma min_id n : min n n == n.
	287	Proof.
	288	apply min_l; order.
	289	Qed.
321	290
322	291	Notation min_idempotent := min_id (only parsing).
323	292
324		Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p.
325		Proof. intros. symmetry; apply MPRev.max_assoc. Qed.
326
327		Lemma min_comm : forall n m, min n m == min m n.
328		Proof. intros. exact (MPRev.max_comm m n). Qed.
329
330		Lemma le_min_r : forall n m, min n m <= m.
331		Proof. intros. exact (MPRev.le_max_l m n). Qed.
332
333		Lemma le_min_l : forall n m, min n m <= n.
334		Proof. intros. exact (MPRev.le_max_r m n). Qed.
335
336		Lemma min_l_iff : forall n m, min n m == n <-> n <= m.
337		Proof. intros n m. exact (MPRev.max_r_iff m n). Qed.
338
339		Lemma min_r_iff : forall n m, min n m == m <-> m <= n.
340		Proof. intros n m. exact (MPRev.max_l_iff m n). Qed.
341
342		Lemma min_le : forall n m p, min n m <= p -> n <= p \/ m <= p.
343		Proof. intros n m p H. destruct (MPRev.max_le _ _ _ H); auto. Qed.
344
345		Lemma min_le_iff : forall n m p, min n m <= p <-> n <= p \/ m <= p.
346		Proof. intros n m p. rewrite (MPRev.max_le_iff m n p); intuition. Qed.
347
348		Lemma min_lt_iff : forall n m p, min n m < p <-> n < p \/ m < p.
349		Proof. intros n m p. rewrite (MPRev.max_lt_iff m n p); intuition. Qed.
350
351		Lemma min_glb_l : forall n m p, p <= min n m -> p <= n.
352		Proof. intros n m. exact (MPRev.max_lub_r m n). Qed.
353
354		Lemma min_glb_r : forall n m p, p <= min n m -> p <= m.
355		Proof. intros n m. exact (MPRev.max_lub_l m n). Qed.
356
357		Lemma min_glb : forall n m p, p <= n -> p <= m -> p <= min n m.
358		Proof. intros. apply MPRev.max_lub; auto. Qed.
359
360		Lemma min_glb_iff : forall n m p, p <= min n m <-> p <= n /\ p <= m.
361		Proof. intros. rewrite (MPRev.max_lub_iff m n p); intuition. Qed.
362
363		Lemma min_glb_lt : forall n m p, p < n -> p < m -> p < min n m.
364		Proof. intros. apply MPRev.max_lub_lt; auto. Qed.
365
366		Lemma min_glb_lt_iff : forall n m p, p < min n m <-> p < n /\ p < m.
367		Proof. intros. rewrite (MPRev.max_lub_lt_iff m n p); intuition. Qed.
368
369		Lemma min_le_compat_l : forall n m p, n <= m -> min p n <= min p m.
370		Proof. intros n m. exact (MPRev.max_le_compat_r m n). Qed.
371
372		Lemma min_le_compat_r : forall n m p, n <= m -> min n p <= min m p.
373		Proof. intros n m. exact (MPRev.max_le_compat_l m n). Qed.
374
375		Lemma min_le_compat : forall n m p q, n <= m -> p <= q ->
	293	Lemma min_assoc m n p : min m (min n p) == min (min m n) p.
	294	Proof.
	295	destruct (min_spec n p) as [(H,E)\|(H,E)]; rewrite E;
	296	destruct (min_spec m n) as [(H',E')\|(H',E')]; rewrite E', ?E; try easy.
	297	- symmetry. apply min_l; order.
	298	- apply min_r; order.
	299	Qed.
	300
	301	Lemma min_comm n m : min n m == min m n.
	302	Proof.
	303	destruct (min_spec m n) as [(H,E)\|(H,E)]; rewrite E;
	304	(apply min_r \|\| apply min_l); order.
	305	Qed.
	306
	307	Ltac solve_min :=
	308	match goal with \|- context [min ?n ?m] =>
	309	destruct (min_spec n m); intuition; order
	310	end.
	311
	312	Lemma le_min_r n m : min n m <= m.
	313	Proof. solve_min. Qed.
	314
	315	Lemma le_min_l n m : min n m <= n.
	316	Proof. solve_min. Qed.
	317
	318	Lemma min_l_iff n m : min n m == n <-> n <= m.
	319	Proof. solve_min. Qed.
	320
	321	Lemma min_r_iff n m : min n m == m <-> m <= n.
	322	Proof. solve_min. Qed.
	323
	324	Lemma min_le n m p : min n m <= p -> n <= p \/ m <= p.
	325	Proof.
	326	destruct (min_spec n m); [left\|right]; intuition; order.
	327	Qed.
	328
	329	Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p.
	330	Proof. split. apply min_le. solve_min. Qed.
	331
	332	Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p.
	333	Proof.
	334	destruct (min_spec n m); intuition;
	335	order \|\| (right; order) \|\| (left; order).
	336	Qed.
	337
	338	Lemma min_glb_l n m p : p <= min n m -> p <= n.
	339	Proof. solve_min. Qed.
	340
	341	Lemma min_glb_r n m p : p <= min n m -> p <= m.
	342	Proof. solve_min. Qed.
	343
	344	Lemma min_glb n m p : p <= n -> p <= m -> p <= min n m.
	345	Proof. solve_min. Qed.
	346
	347	Lemma min_glb_iff n m p : p <= min n m <-> p <= n /\ p <= m.
	348	Proof. solve_min. Qed.
	349
	350	Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m.
	351	Proof. solve_min. Qed.
	352
	353	Lemma min_glb_lt_iff n m p : p < min n m <-> p < n /\ p < m.
	354	Proof. solve_min. Qed.
	355
	356	Lemma min_le_compat_l n m p : n <= m -> min p n <= min p m.
	357	Proof. intros. apply min_glb_iff. solve_min. Qed.
	358
	359	Lemma min_le_compat_r n m p : n <= m -> min n p <= min m p.
	360	Proof. intros. apply min_glb_iff. solve_min. Qed.
	361
	362	Lemma min_le_compat n m p q : n <= m -> p <= q ->
376	363	min n p <= min m q.
377		Proof. intros. apply MPRev.max_le_compat; auto. Qed.
378
	364	Proof.
	365	intros Hnm Hpq.
	366	assert (LE := min_le_compat_l _ _ m Hpq).
	367	assert (LE' := min_le_compat_r _ _ p Hnm).
	368	order.
	369	Qed.
379	370
380	371	( * Combined properties of min and max *)
381	372
382		Lemma min_max_absorption : forall n m, max n (min n m) == n.
	373	Lemma min_max_absorption n m : max n (min n m) == n.
383	374	Proof.
384	375	intros.
385	376	destruct (min_spec n m) as [(C,E)\|(C,E)]; rewrite E.

387	378	destruct (max_spec n m); intuition; order.
388	379	Qed.
389	380
390		Lemma max_min_absorption : forall n m, min n (max n m) == n.
	381	Lemma max_min_absorption n m : min n (max n m) == n.
391	382	Proof.
392	383	intros.
393	384	destruct (max_spec n m) as [(C,E)\|(C,E)]; rewrite E.

397	388
398	389	(** Distributivity *)
399	390
400		Lemma max_min_distr : forall n m p,
	391	Lemma max_min_distr n m p :
401	392	max n (min m p) == min (max n m) (max n p).
402	393	Proof.
403		intros. symmetry. apply min_mono.
	394	symmetry. apply min_mono.
404	395	eauto with *.
405	396	repeat red; intros. apply max_le_compat_l; auto.
406	397	Qed.
407	398
408		Lemma min_max_distr : forall n m p,
	399	Lemma min_max_distr n m p :
409	400	min n (max m p) == max (min n m) (min n p).
410	401	Proof.
411		intros. symmetry. apply max_mono.
	402	symmetry. apply max_mono.
412	403	eauto with *.
413	404	repeat red; intros. apply min_le_compat_l; auto.
414	405	Qed.
415	406
416	407	(** Modularity *)
417	408
418		Lemma max_min_modular : forall n m p,
	409	Lemma max_min_modular n m p :
419	410	max n (min m (max n p)) == min (max n m) (max n p).
420	411	Proof.
421		intros. rewrite <- max_min_distr.
	412	rewrite <- max_min_distr.
422	413	destruct (max_spec n p) as [(C,E)\|(C,E)]; rewrite E; auto with *.
423	414	destruct (min_spec m n) as [(C',E')\|(C',E')]; rewrite E'.
424	415	rewrite 2 max_l; try order. rewrite min_le_iff; auto.
425	416	rewrite 2 max_l; try order. rewrite min_le_iff; auto.
426	417	Qed.
427	418
428		Lemma min_max_modular : forall n m p,
	419	Lemma min_max_modular n m p :
429	420	min n (max m (min n p)) == max (min n m) (min n p).
430	421	Proof.
431	422	intros. rewrite <- min_max_distr.

437	428
438	429	(** Disassociativity *)
439	430
440		Lemma max_min_disassoc : forall n m p,
	431	Lemma max_min_disassoc n m p :
441	432	min n (max m p) <= max (min n m) p.
442	433	Proof.
443	434	intros. rewrite min_max_distr.

446	437
447	438	(** Anti-monotonicity swaps the role of [min] and [max] *)
448	439
449		Lemma max_min_antimono : forall f,
	440	Lemma max_min_antimono f :
450	441	Proper (eq==>eq) f ->
451	442	Proper (le==>inverse le) f ->
452	443	forall x y, max (f x) (f y) == f (min x y).
453	444	Proof.
454		intros f Eqf Lef x y.
	445	intros Eqf Lef x y.
455	446	destruct (min_spec x y) as [(H,E)\|(H,E)]; rewrite E;
456	447	destruct (max_spec (f x) (f y)) as [(H',E')\|(H',E')]; auto.
457	448	assert (f y <= f x) by (apply Lef; order). order.
458	449	assert (f x <= f y) by (apply Lef; order). order.
459	450	Qed.
460	451
461		Lemma min_max_antimono : forall f,
	452	Lemma min_max_antimono f :
462	453	Proper (eq==>eq) f ->
463	454	Proper (le==>inverse le) f ->
464	455	forall x y, min (f x) (f y) == f (max x y).
465	456	Proof.
466		intros f Eqf Lef x y.
	457	intros Eqf Lef x y.
467	458	destruct (max_spec x y) as [(H,E)\|(H,E)]; rewrite E;
468	459	destruct (min_spec (f x) (f y)) as [(H',E')\|(H',E')]; auto.
469	460	assert (f y <= f x) by (apply Lef; order). order.

479	470
480	471	(** Induction principles for [max]. *)
481	472
482		Lemma max_case_strong : forall n m (P:t -> Type),
	473	Lemma max_case_strong n m (P:t -> Type) :
483	474	(forall x y, x==y -> P x -> P y) ->
484	475	(m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
485	476	Proof.
486		intros n m P Compat Hl Hr.
	477	intros Compat Hl Hr.
487	478	destruct (CompSpec2Type (compare_spec n m)) as [EQ\|LT\|GT].
488	479	assert (n<=m) by (rewrite le_lteq; auto).
489	480	apply (Compat m), Hr; auto. symmetry; apply max_r; auto.

493	484	apply (Compat n), Hl; auto. symmetry; apply max_l; auto.
494	485	Defined.
495	486
496		Lemma max_case : forall n m (P:t -> Type),
	487	Lemma max_case n m (P:t -> Type) :
497	488	(forall x y, x == y -> P x -> P y) ->
498	489	P n -> P m -> P (max n m).
499	490	Proof. intros. apply max_case_strong; auto. Defined.
500	491
501	492	(** [max] returns one of its arguments. *)
502	493
503		Lemma max_dec : forall n m, {max n m == n} + {max n m == m}.
504		Proof.
505		intros n m. apply max_case; auto with relations.
	494	Lemma max_dec n m : {max n m == n} + {max n m == m}.
	495	Proof.
	496	apply max_case; auto with relations.
506	497	intros x y H [E\|E]; [left\|right]; rewrite <-H; auto.
507	498	Defined.
508	499
509	500	(** Idem for [min] *)
510	501
511		Lemma min_case_strong : forall n m (P:O.t -> Type),
	502	Lemma min_case_strong n m (P:O.t -> Type) :
512	503	(forall x y, x == y -> P x -> P y) ->
513	504	(n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
514	505	Proof.
515		intros n m P Compat Hl Hr.
	506	intros Compat Hl Hr.
516	507	destruct (CompSpec2Type (compare_spec n m)) as [EQ\|LT\|GT].
517	508	assert (n<=m) by (rewrite le_lteq; auto).
518	509	apply (Compat n), Hl; auto. symmetry; apply min_l; auto.

522	513	apply (Compat m), Hr; auto. symmetry; apply min_r; auto.
523	514	Defined.
524	515
525		Lemma min_case : forall n m (P:O.t -> Type),
	516	Lemma min_case n m (P:O.t -> Type) :
526	517	(forall x y, x == y -> P x -> P y) ->
527	518	P n -> P m -> P (min n m).
528	519	Proof. intros. apply min_case_strong; auto. Defined.
529	520
530		Lemma min_dec : forall n m, {min n m == n} + {min n m == m}.
	521	Lemma min_dec n m : {min n m == n} + {min n m == m}.
531	522	Proof.
532	523	intros. apply min_case; auto with relations.
533	524	intros x y H [E\|E]; [left\|right]; rewrite <- E; auto with relations.

557	548
558	549	Include MinMaxLogicalProperties O M.
559	550
560		Lemma max_monotone : forall f, Proper (le ==> le) f ->
	551	Lemma max_monotone f : Proper (le ==> le) f ->
561	552	forall x y, max (f x) (f y) = f (max x y).
562	553	Proof. intros; apply max_mono; auto. congruence. Qed.
563	554
564		Lemma min_monotone : forall f, Proper (le ==> le) f ->
	555	Lemma min_monotone f : Proper (le ==> le) f ->
565	556	forall x y, min (f x) (f y) = f (min x y).
566	557	Proof. intros; apply min_mono; auto. congruence. Qed.
567	558
568		Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f ->
	559	Lemma min_max_antimonotone f : Proper (le ==> inverse le) f ->
569	560	forall x y, min (f x) (f y) = f (max x y).
570	561	Proof. intros; apply min_max_antimono; auto. congruence. Qed.
571	562
572		Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f ->
	563	Lemma max_min_antimonotone f : Proper (le ==> inverse le) f ->
573	564	forall x y, max (f x) (f y) = f (min x y).
574	565	Proof. intros; apply max_min_antimono; auto. congruence. Qed.
575	566

+15

-13

theories/Structures/OrderedType.v less more

107	107	Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
108	108	Proof. intros; destruct (compare x y); auto. Qed.
109	109
110		Module OrderElts <: Orders.TotalOrder.
111		Definition t := t.
112		Definition eq := eq.
113		Definition lt := lt.
114		Definition le x y := lt x y \/ eq x y.
115		Definition eq_equiv := eq_equiv.
116		Definition lt_strorder := lt_strorder.
117		Definition lt_compat := lt_compat.
118		Definition lt_total := lt_total.
119		Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
120		Proof. unfold le; intuition. Qed.
121		End OrderElts.
122		Module OrderTac := !MakeOrderTac OrderElts.
	110	Module TO.
	111	Definition t := t.
	112	Definition eq := eq.
	113	Definition lt := lt.
	114	Definition le x y := lt x y \/ eq x y.
	115	End TO.
	116	Module IsTO.
	117	Definition eq_equiv := eq_equiv.
	118	Definition lt_strorder := lt_strorder.
	119	Definition lt_compat := lt_compat.
	120	Definition lt_total := lt_total.
	121	Lemma le_lteq x y : TO.le x y <-> lt x y \/ eq x y.
	122	Proof. reflexivity. Qed.
	123	End IsTO.
	124	Module OrderTac := !MakeOrderTac TO IsTO.
123	125	Ltac order := OrderTac.order.
124	126
125	127	Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed.

+27

-44

theories/Structures/OrdersTac.v less more

39	39	Local Infix "+" := trans_ord.
40	40
41	41
42		( The requirements of the tactic : [TotalOrder].
43
44		[TotalOrder] contains an equivalence [eq],
45		a strict order [lt] total and compatible with [eq], and
46		a larger order [le] synonym for [lt\/eq].
	42	( The tactic requirements : a total order
	43
	44	We need :
	45	- an equivalence [eq],
	46	- a strict order [lt] total and compatible with [eq],
	47	- a larger order [le] synonym for [lt\/eq].
	48
	49	This used to be provided here via a [TotalOrder], but
	50	for technical reasons related to extraction, we now ask
	51	for two sperate parts: relations in a [EqLtLe] + properties in
	52	[IsTotalOrder]. Note that [TotalOrder = EqLtLe <+ IsTotalOrder]
47	53	*)
48	54
	55	Module Type IsTotalOrder (O:EqLtLe) :=
	56	IsEq O <+ IsStrOrder O <+ LeIsLtEq O <+ LtIsTotal O.
	57
49	58	( Properties that will be used by the [order] tactic *)
50	59
51		Module OrderFacts(Import O:TotalOrder').
	60	Module OrderFacts (Import O:EqLtLe)(P:IsTotalOrder O).
	61	Include EqLtLeNotation O.
52	62
53	63	(** Reflexivity rules *)
54	64

56	66	Proof. reflexivity. Qed.
57	67
58	68	Lemma le_refl : forall x, x<=x.
59		Proof. intros; rewrite le_lteq; right; reflexivity. Qed.
	69	Proof. intros; rewrite P.le_lteq; right; reflexivity. Qed.
60	70
61	71	Lemma lt_irrefl : forall x, ~ x<x.
62	72	Proof. intros; apply StrictOrder_Irreflexive. Qed.

68	78
69	79	Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y.
70	80	Proof.
71		intros x y; rewrite 2 le_lteq. intuition.
	81	intros x y; rewrite 2 P.le_lteq. intuition.
72	82	elim (StrictOrder_Irreflexive x); transitivity y; auto.
73	83	Qed.
74	84

89	99
90	100	Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
91	101	Proof.
92		destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition;
	102	destruct o, o'; simpl; intros x y z; rewrite ?P.le_lteq; intuition;
93	103	subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
94	104	Qed.
95	105

113	123
114	124	Lemma not_neq_eq : forall x y, ~~x==y -> x==y.
115	125	Proof.
116		intros x y H. destruct (lt_total x y) as [H'\|[H'\|H']]; auto;
	126	intros x y H. destruct (P.lt_total x y) as [H'\|[H'\|H']]; auto;
117	127	destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto.
118	128	Qed.
119	129
120	130	Lemma not_ge_lt : forall x y, ~y<=x -> x<y.
121	131	Proof.
122		intros x y H. destruct (lt_total x y); auto.
123		destruct H. rewrite le_lteq. intuition.
	132	intros x y H. destruct (P.lt_total x y); auto.
	133	destruct H. rewrite P.le_lteq. intuition.
124	134	Qed.
125	135
126	136	Lemma not_gt_le : forall x y, ~y<x -> x<=y.
127	137	Proof.
128		intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition.
	138	intros x y H. rewrite P.le_lteq. generalize (P.lt_total x y); intuition.
129	139	Qed.
130	140
131	141	Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y.

137	147
138	148	( [MakeOrderTac] : The functor providing the order tactic. *)
139	149
140		Module MakeOrderTac (Import O:TotalOrder').
141
142		Include OrderFacts O.
	150	Module MakeOrderTac (Import O:EqLtLe)(P:IsTotalOrder O).
	151	Include OrderFacts O P.
	152	Include EqLtLeNotation O.
143	153
144	154	(** order_eq : replace x by y in all (in)equations hyps thanks
145	155	to equality EQ (where eq has been hidden in order to avoid

256	266
257	267	Module OTF_to_OrderTac (OTF:OrderedTypeFull).
258	268	Module TO := OTF_to_TotalOrder OTF.
259		Include !MakeOrderTac TO.
	269	Include !MakeOrderTac OTF TO.
260	270	End OTF_to_OrderTac.
261	271
262	272	Module OT_to_OrderTac (OT:OrderedType).
263	273	Module OTF := OT_to_Full OT.
264	274	Include !OTF_to_OrderTac OTF.
265	275	End OT_to_OrderTac.
266
267		Module TotalOrderRev (O:TotalOrder) <: TotalOrder.
268
269		Definition t := O.t.
270		Definition eq := O.eq.
271		Definition lt := flip O.lt.
272		Definition le := flip O.le.
273		Include EqLtLeNotation.
274
275		(* No Instance syntax to avoid saturating the Equivalence tables *)
276		Definition eq_equiv := O.eq_equiv.
277
278		Instance lt_strorder: StrictOrder lt.
279		Proof. unfold lt; auto with *. Qed.
280		Instance lt_compat : Proper (eq==>eq==>iff) lt.
281		Proof. unfold lt; auto with *. Qed.
282
283		Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
284		Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
285
286		Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
287		Proof.
288		intros x y; unfold lt, eq, flip.
289		generalize (O.lt_total x y); intuition.
290		Qed.
291
292		End TotalOrderRev.

+1

-5

theories/ZArith/Int.v less more

23	23
24	24	Parameter t : Set.
25	25	Bind Scope Int_scope with t.
26
27		(** For compatibility *)
28		Definition int := t.
29	26
30	27	Parameter i2z : t -> Z.
31	28

361	358	Module Z_as_Int <: Int.
362	359	Local Open Scope Z_scope.
363	360	Definition t := Z.
364		Definition int := t.
365	361	Definition _0 := 0.
366	362	Definition _1 := 1.
367	363	Definition _2 := 2.

374	370	Definition gt_le_dec := Z_gt_le_dec.
375	371	Definition ge_lt_dec := Z_ge_lt_dec.
376	372	Definition eq_dec := Z.eq_dec.
377		Definition i2z : int -> Z := fun n => n.
	373	Definition i2z : t -> Z := fun n => n.
378	374	Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed.
379	375	Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed.
380	376	Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed.

+10

-6

tools/coq_makefile.ml less more

221	221	print "\n";
222	222	end;
223	223	print "install:";
224		if (not_empty cmxsfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)";
	224	if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)";
225	225	print "\n";
226	226	if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc;
227	227	if (not_empty cmofiles) then

290	290	print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
291	291	print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
292	292	print "%.ml4.d: %.ml4\n";
293		print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" \|\| ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
	293	print "\t$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" \|\| ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
294	294	let ml_rules () =
295	295	print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
296	296	print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
297	297	print "%.ml.d: %.ml\n";
298	298	print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" \|\| ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
299	299	let cmxs_rules () =
	300	print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n";
300	301	print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n" in
301	302	let mllib_rules () =
302	303	print "%.cma: \| %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
303	304	print "%.cmxa: \| %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
304		print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n";
305	305	print "%.mllib.d: %.mllib\n";
306	306	print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" \|\| ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
307	307	let mlpack_rules () =

410	410	print "# DSTROOT to specify a prefix to install path.\n\n";
411	411	print "# Here is a hack to make $(eval $(shell works:\n";
412	412	print "define donewline\n\n\nendef\n";
413		print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) \| tr '\\n' '@'; })))\n";
	413	print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) \| tr -d '\\r' \| tr '\\n' '@'; })))\n";
414	414	print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"
415	415
416	416	let include_dirs (inc_i,inc_r) =

542	542	print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n";
543	543	classify_files_by_root "CMXSFILES" (l1@l2) inc;
544	544	end;
545		print "\n";
	545	print "ifeq '$(HASNATDYNLINK)' 'true'\n";
	546	print "HASNATDYNLINK_OR_EMPTY := yes\n";
	547	print "else\n";
	548	print "HASNATDYNLINK_OR_EMPTY :=\n";
	549	print "endif\n\n";
546	550	section "Definition of the toplevel targets.";
547	551	print "all: ";
548	552	if !some_vfile then print "$(VOFILES) ";
549	553	if !some_mlfile \|\| !some_ml4file \|\| !some_mlpackfile then print "$(CMOFILES) ";
550	554	if !some_mllibfile then print "$(CMAFILES) ";
551	555	if !some_mlfile \|\| !some_ml4file \|\| !some_mllibfile \|\| !some_mlpackfile
552		then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) ";
	556	then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) ";
553	557	print_list "\\\n " other_targets; print "\n\n";
554	558	if !some_mlifile then
555	559	begin

+295

-0

tools/coq_tex.ml less more

	0	(************************************************************************)
	1	(* v * The Coq Proof Assistant / The Coq Development Team *)
	2	(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
	3	(* \VV/ **************************************************************)
	4	(* // * This file is distributed under the terms of the *)
	5	(* * GNU Lesser General Public License Version 2.1 *)
	6	(************************************************************************)
	7
	8	(* coq-tex
	9	* JCF, 16/1/98
	10	* adapted from caml-tex (perl script written by Xavier Leroy)
	11	*
	12	* Perl isn't as portable as it pretends to be, and is quite difficult
	13	* to read and maintain... Let us rewrite the stuff in Caml! *)
	14
	15	let linelen = ref 72
	16	let output = ref ""
	17	let output_specified = ref false
	18	let image = ref ""
	19	let cut_at_blanks = ref false
	20	let verbose = ref false
	21	let slanted = ref false
	22	let hrule = ref false
	23	let small = ref false
	24	let boot = ref false
	25
	26	let coq_prompt = Str.regexp "Coq < "
	27	let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
	28
	29	let remove_prompt s = Str.replace_first any_prompt "" s
	30
	31	(* First pass: extract the Coq phrases to evaluate from [texfile]
	32	* and put them into the file [inputv] *)
	33
	34	let begin_coq = Str.regexp "\\\\begin{coq_\$example\\\|example\\\\\|example\\#\\\|eval\$}[ \t]$"
	35	let end_coq = Str.regexp "\\\\end{coq_\$example\\\|example\\\\\|example\\#\\\|eval\$}[ \t]$"
	36
	37	let extract texfile inputv =
	38	let chan_in = open_in texfile in
	39	let chan_out = open_out inputv in
	40	let rec inside () =
	41	let s = input_line chan_in in
	42	if Str.string_match end_coq s 0 then
	43	outside ()
	44	else begin
	45	output_string chan_out (s ^ "\n");
	46	inside ()
	47	end
	48	and outside () =
	49	let s = input_line chan_in in
	50	if Str.string_match begin_coq s 0 then
	51	inside ()
	52	else
	53	outside ()
	54	in
	55	try
	56	output_string chan_out
	57	("Set Printing Width " ^ (string_of_int !linelen) ^".\n");
	58	outside ()
	59	with End_of_file ->
	60	begin close_in chan_in; close_out chan_out end
	61
	62	(* Second pass: insert the answers of Coq from [coq_output] into the
	63	* TeX file [texfile]. The result goes in file [result]. *)
	64
	65	let begin_coq_example =
	66	Str.regexp "\\\\begin{coq_\$example\\\|example\\\\\|example\\#\$}[ \t]$"
	67	let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
	68	let end_coq_example = Str.regexp "\\\\end{coq_\$example\\\|example\\\\\|example\\#\$}[ \t]$"
	69	let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
	70	let dot_end_line = Str.regexp "\\.[ \t]\$(\\.\\)\$?[ \t]*$"
	71
	72	let has_match r s =
	73	try let _ = Str.search_forward r s 0 in true with Not_found -> false
	74
	75	let percent = Str.regexp "%"
	76	let bang = Str.regexp "!"
	77	let expos = Str.regexp "^"
	78
	79	let tex_escaped s =
	80	let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in
	81	let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in
	82	let adapt_delim = function
	83	\| "_" \| "{" \| "}" \| "&" \| "%" \| "#" \| "$" as c -> "\\"^c
	84	\| "\\" -> "{\\char'134}"
	85	\| "^" -> "{\\char'136}"
	86	\| "~" -> "{\\char'176}"
	87	\| " " -> "~"
	88	\| "<" -> "{<}"
	89	\| ">" -> "{>}"
	90	\| _ -> assert false
	91	in
	92	let adapt = function
	93	\| Str.Text s -> s
	94	\| Str.Delim s -> adapt_delim s
	95	in
	96	String.concat "" (List.map adapt (Str.full_split delims s))
	97
	98	let encapsule sl c_out s =
	99	if sl then
	100	Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s)
	101	else
	102	Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s)
	103
	104	let print_block c_out bl =
	105	List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl
	106
	107	let insert texfile coq_output result =
	108	let c_tex = open_in texfile in
	109	let c_coq = open_in coq_output in
	110	let c_out = open_out result in
	111	(* next_block k : this function reads the next block of Coq output
	112	* removing the k leading prompts.
	113	* it returns the block as a list of string) *)
	114	let last_read = ref "" in
	115	let next_block k =
	116	if !last_read = "" then last_read := input_line c_coq;
	117	(* skip k prompts *)
	118	for i = 1 to k do
	119	last_read := remove_prompt !last_read;
	120	done;
	121	(* read and return the following lines until a prompt is found *)
	122	let rec read_lines () =
	123	let s = input_line c_coq in
	124	if Str.string_match any_prompt s 0 then begin
	125	last_read := s; []
	126	end else
	127	s :: (read_lines ())
	128	in
	129	let first = !last_read in first :: (read_lines ())
	130	in
	131	(* we are just after \end{coq_...} block *)
	132	let rec just_after () =
	133	let s = input_line c_tex in
	134	if Str.string_match begin_coq_example s 0 then begin
	135	inside (Str.matched_group 1 s <> "example*")
	136	(Str.matched_group 1 s <> "example#") 0 false
	137	end
	138	else begin
	139	if !hrule then output_string c_out "\\hrulefill\\\\\n";
	140	output_string c_out "\\end{flushleft}\n";
	141	if !small then output_string c_out "\\end{small}\n";
	142	if Str.string_match begin_coq_eval s 0 then
	143	eval 0
	144	else begin
	145	output_string c_out (s ^ "\n");
	146	outside ()
	147	end
	148	end
	149	(* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
	150	and outside () =
	151	let s = input_line c_tex in
	152	if Str.string_match begin_coq_example s 0 then begin
	153	if !small then output_string c_out "\\begin{small}\n";
	154	output_string c_out "\\begin{flushleft}\n";
	155	if !hrule then output_string c_out "\\hrulefill\\\\\n";
	156	inside (Str.matched_group 1 s <> "example*")
	157	(Str.matched_group 1 s <> "example#") 0 true
	158	end else if Str.string_match begin_coq_eval s 0 then
	159	eval 0
	160	else begin
	161	output_string c_out (s ^ "\n");
	162	outside ()
	163	end
	164	(* we are inside a \begin{coq_example?} ... \end{coq_example?} block
	165	* show_answers tells what kind of block it is
	166	* k is the number of lines read until now *)
	167	and inside show_answers show_questions k first_block =
	168	let s = input_line c_tex in
	169	if Str.string_match end_coq_example s 0 then begin
	170	just_after ()
	171	end else begin
	172	if !verbose then Printf.printf "Coq < %s\n" s;
	173	if (not first_block) & k=0 then output_string c_out "\\medskip\n";
	174	if show_questions then encapsule false c_out ("Coq < " ^ s);
	175	if has_match dot_end_line s then begin
	176	let bl = next_block (succ k) in
	177	if !verbose then List.iter print_endline bl;
	178	if show_answers then print_block c_out bl;
	179	inside show_answers show_questions 0 false
	180	end else
	181	inside show_answers show_questions (succ k) first_block
	182	end
	183	(* we are inside a \begin{coq_eval} ... \end{coq_eval} block
	184	* k is the number of lines read until now *)
	185	and eval k =
	186	let s = input_line c_tex in
	187	if Str.string_match end_coq_eval s 0 then
	188	outside ()
	189	else begin
	190	if !verbose then Printf.printf "Coq < %s\n" s;
	191	if has_match dot_end_line s then
	192	let bl = next_block (succ k) in
	193	if !verbose then List.iter print_endline bl;
	194	eval 0
	195	else
	196	eval (succ k)
	197	end
	198	in
	199	try
	200	let _ = next_block 0 in (* to skip the Coq banner *)
	201	let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *)
	202	outside ()
	203	with End_of_file -> begin
	204	close_in c_tex;
	205	close_in c_coq;
	206	close_out c_out
	207	end
	208
	209	(* Process of one TeX file *)
	210
	211	let rm f = try Sys.remove f with _ -> ()
	212
	213	let one_file texfile =
	214	let inputv = Filename.temp_file "coq_tex" ".v" in
	215	let coq_output = Filename.temp_file "coq_tex" ".coq_output"in
	216	let result =
	217	if !output_specified then
	218	!output
	219	else if Filename.check_suffix texfile ".tex" then
	220	(Filename.chop_suffix texfile ".tex") ^ ".v.tex"
	221	else
	222	texfile ^ ".v.tex"
	223	in
	224	try
	225	(* 1. extract Coq phrases *)
	226	extract texfile inputv;
	227	(* 2. run Coq on input *)
	228	let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv
	229	coq_output)
	230	in
	231	(* 3. insert Coq output into original file *)
	232	insert texfile coq_output result;
	233	(* 4. clean up *)
	234	rm inputv; rm coq_output
	235	with e -> begin
	236	rm inputv; rm coq_output;
	237	raise e
	238	end
	239
	240	(* Parsing of the command line, check of the Coq command and process
	241	* of all the files in the command line, one by one *)
	242
	243	let files = ref []
	244
	245	let parse_cl () =
	246	Arg.parse
	247	[ "-o", Arg.String (fun s -> output_specified := true; output := s),
	248	"output-file Specifiy the resulting LaTeX file";
	249	"-n", Arg.Int (fun n -> linelen := n),
	250	"line-width Set the line width";
	251	"-image", Arg.String (fun s -> image := s),
	252	"coq-image Use coq-image as Coq command";
	253	"-w", Arg.Set cut_at_blanks,
	254	" Try to cut lines at blanks";
	255	"-v", Arg.Set verbose,
	256	" Verbose mode (show Coq answers on stdout)";
	257	"-sl", Arg.Set slanted,
	258	" Coq answers in slanted font (only with LaTeX2e)";
	259	"-hrule", Arg.Set hrule,
	260	" Coq parts are written between 2 horizontal lines";
	261	"-small", Arg.Set small,
	262	" Coq parts are written in small font";
	263	"-boot", Arg.Set boot,
	264	" Launch coqtop with the -boot option"
	265	]
	266	(fun s -> files := s :: !files)
	267	"coq-tex [options] file ..."
	268
	269	let find_coqtop () =
	270	let prog = Sys.executable_name in
	271	try
	272	let size = String.length prog in
	273	let i = Str.search_backward (Str.regexp_string "coq-tex") prog (size-7) in
	274	(String.sub prog 0 i)^"coqtop"^(String.sub prog (i+7) (size-i-7))
	275	with Not_found -> begin
	276	Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
	277	"coqtop"
	278	end
	279
	280	let main () =
	281	parse_cl ();
	282	if !image = "" then image := Filename.quote (find_coqtop ());
	283	if !boot then image := !image ^ " -boot";
	284	if Sys.command (!image ^ " -batch -silent") <> 0 then begin
	285	Printf.printf "Error: ";
	286	let _ = Sys.command (!image ^ " -batch") in
	287	exit 1
	288	end else begin
	289	Printf.printf "Your version of coqtop seems OK\n";
	290	flush stdout
	291	end;
	292	List.iter one_file (List.rev !files)
	293
	294	let _ = Printexc.catch main ()

+0

-290

~~tools/coq_tex.ml4~~ less more

0		(************************************************************************)
1		(* v * The Coq Proof Assistant / The Coq Development Team *)
2		(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
3		(* \VV/ **************************************************************)
4		(* // * This file is distributed under the terms of the *)
5		(* * GNU Lesser General Public License Version 2.1 *)
6		(************************************************************************)
7
8		(* coq-tex
9		* JCF, 16/1/98
10		* adapted from caml-tex (perl script written by Xavier Leroy)
11		*
12		* Perl isn't as portable as it pretends to be, and is quite difficult
13		* to read and maintain... Let us rewrite the stuff in Caml! *)
14
15		let _ =
16		match Sys.os_type with
17		\| "Unix" -> ()
18		\| _ -> begin
19		print_string "This program only runs under Unix !\n";
20		flush stdout;
21		exit 1
22		end
23
24		let linelen = ref 72
25		let output = ref ""
26		let output_specified = ref false
27		let image = ref ""
28		let cut_at_blanks = ref false
29		let verbose = ref false
30		let slanted = ref false
31		let hrule = ref false
32		let small = ref false
33
34		let coq_prompt = Str.regexp "Coq < "
35		let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
36
37		let remove_prompt s = Str.replace_first any_prompt "" s
38
39		(* First pass: extract the Coq phrases to evaluate from [texfile]
40		* and put them into the file [inputv] *)
41
42		let begin_coq = Str.regexp "\\\\begin{coq_\$example\\\|example\\\\\|example\\#\\\|eval\$}[ \t]$"
43		let end_coq = Str.regexp "\\\\end{coq_\$example\\\|example\\\\\|example\\#\\\|eval\$}[ \t]$"
44
45		let extract texfile inputv =
46		let chan_in = open_in texfile in
47		let chan_out = open_out inputv in
48		let rec inside () =
49		let s = input_line chan_in in
50		if Str.string_match end_coq s 0 then
51		outside ()
52		else begin
53		output_string chan_out (s ^ "\n");
54		inside ()
55		end
56		and outside () =
57		let s = input_line chan_in in
58		if Str.string_match begin_coq s 0 then
59		inside ()
60		else
61		outside ()
62		in
63		try
64		output_string chan_out
65		("Set Printing Width " ^ (string_of_int !linelen) ^".\n");
66		outside ()
67		with End_of_file ->
68		begin close_in chan_in; close_out chan_out end
69
70		(* Second pass: insert the answers of Coq from [coq_output] into the
71		* TeX file [texfile]. The result goes in file [result]. *)
72
73		let begin_coq_example =
74		Str.regexp "\\\\begin{coq_\$example\\\|example\\\\\|example\\#\$}[ \t]$"
75		let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
76		let end_coq_example = Str.regexp "\\\\end{coq_\$example\\\|example\\\\\|example\\#\$}[ \t]$"
77		let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
78		let dot_end_line = Str.regexp "\\.[ \t]\$(\\.\\)\$?[ \t]*$"
79
80		let has_match r s =
81		try let _ = Str.search_forward r s 0 in true with Not_found -> false
82
83		let percent = Str.regexp "%"
84		let bang = Str.regexp "!"
85		let expos = Str.regexp "^"
86
87		let tex_escaped s =
88		let rec trans = parser
89		\| [< s1 = (parser
90		\| [< ''_'\|'$'\|'{'\|'}'\|'&'\|'%'\|'#' as c >] ->
91		"\\" ^ (String.make 1 c)
92		\| [< ''\\' >] -> "{\\char'134}"
93		\| [< ''^' >] -> "{\\char'136}"
94		\| [< ''~' >] -> "{\\char'176}"
95		\| [< '' ' >] -> "~"
96		\| [< ''<' >] -> "{<}"
97		\| [< ''>' >] -> "{>}"
98		\| [< 'c >] -> String.make 1 c);
99		s2 = trans >] -> s1 ^ s2
100		\| [< >] -> ""
101		in
102		trans (Stream.of_string s)
103
104		let encapsule sl c_out s =
105		if sl then
106		Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s)
107		else
108		Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s)
109
110		let print_block c_out bl =
111		List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl
112
113		let insert texfile coq_output result =
114		let c_tex = open_in texfile in
115		let c_coq = open_in coq_output in
116		let c_out = open_out result in
117		(* next_block k : this function reads the next block of Coq output
118		* removing the k leading prompts.
119		* it returns the block as a list of string) *)
120		let last_read = ref "" in
121		let next_block k =
122		if !last_read = "" then last_read := input_line c_coq;
123		(* skip k prompts *)
124		for i = 1 to k do
125		last_read := remove_prompt !last_read;
126		done;
127		(* read and return the following lines until a prompt is found *)
128		let rec read_lines () =
129		let s = input_line c_coq in
130		if Str.string_match any_prompt s 0 then begin
131		last_read := s; []
132		end else
133		s :: (read_lines ())
134		in
135		let first = !last_read in first :: (read_lines ())
136		in
137		(* we are just after \end{coq_...} block *)
138		let rec just_after () =
139		let s = input_line c_tex in
140		if Str.string_match begin_coq_example s 0 then begin
141		inside (Str.matched_group 1 s <> "example*")
142		(Str.matched_group 1 s <> "example#") 0 false
143		end
144		else begin
145		if !hrule then output_string c_out "\\hrulefill\\\\\n";
146		output_string c_out "\\end{flushleft}\n";
147		if !small then output_string c_out "\\end{small}\n";
148		if Str.string_match begin_coq_eval s 0 then
149		eval 0
150		else begin
151		output_string c_out (s ^ "\n");
152		outside ()
153		end
154		end
155		(* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
156		and outside () =
157		let s = input_line c_tex in
158		if Str.string_match begin_coq_example s 0 then begin
159		if !small then output_string c_out "\\begin{small}\n";
160		output_string c_out "\\begin{flushleft}\n";
161		if !hrule then output_string c_out "\\hrulefill\\\\\n";
162		inside (Str.matched_group 1 s <> "example*")
163		(Str.matched_group 1 s <> "example#") 0 true
164		end else if Str.string_match begin_coq_eval s 0 then
165		eval 0
166		else begin
167		output_string c_out (s ^ "\n");
168		outside ()
169		end
170		(* we are inside a \begin{coq_example?} ... \end{coq_example?} block
171		* show_answers tells what kind of block it is
172		* k is the number of lines read until now *)
173		and inside show_answers show_questions k first_block =
174		let s = input_line c_tex in
175		if Str.string_match end_coq_example s 0 then begin
176		just_after ()
177		end else begin
178		if !verbose then Printf.printf "Coq < %s\n" s;
179		if (not first_block) & k=0 then output_string c_out "\\medskip\n";
180		if show_questions then encapsule false c_out ("Coq < " ^ s);
181		if has_match dot_end_line s then begin
182		let bl = next_block (succ k) in
183		if !verbose then List.iter print_endline bl;
184		if show_answers then print_block c_out bl;
185		inside show_answers show_questions 0 false
186		end else
187		inside show_answers show_questions (succ k) first_block
188		end
189		(* we are inside a \begin{coq_eval} ... \end{coq_eval} block
190		* k is the number of lines read until now *)
191		and eval k =
192		let s = input_line c_tex in
193		if Str.string_match end_coq_eval s 0 then
194		outside ()
195		else begin
196		if !verbose then Printf.printf "Coq < %s\n" s;
197		if has_match dot_end_line s then
198		let bl = next_block (succ k) in
199		if !verbose then List.iter print_endline bl;
200		eval 0
201		else
202		eval (succ k)
203		end
204		in
205		try
206		let _ = next_block 0 in (* to skip the Coq banner *)
207		let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *)
208		outside ()
209		with End_of_file -> begin
210		close_in c_tex;
211		close_in c_coq;
212		close_out c_out
213		end
214
215		(* Process of one TeX file *)
216
217		let rm f = try Sys.remove f with _ -> ()
218
219		let one_file texfile =
220		let inputv = Filename.temp_file "coq_tex" ".v" in
221		let coq_output = Filename.temp_file "coq_tex" ".coq_output"in
222		let result =
223		if !output_specified then
224		!output
225		else if Filename.check_suffix texfile ".tex" then
226		(Filename.chop_suffix texfile ".tex") ^ ".v.tex"
227		else
228		texfile ^ ".v.tex"
229		in
230		try
231		(* 1. extract Coq phrases *)
232		extract texfile inputv;
233		(* 2. run Coq on input *)
234		let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv
235		coq_output)
236		in
237		(* 3. insert Coq output into original file *)
238		insert texfile coq_output result;
239		(* 4. clean up *)
240		rm inputv; rm coq_output
241		with e -> begin
242		rm inputv; rm coq_output;
243		raise e
244		end
245
246		(* Parsing of the command line, check of the Coq command and process
247		* of all the files in the command line, one by one *)
248
249		let files = ref []
250
251		let parse_cl () =
252		Arg.parse
253		[ "-o", Arg.String (fun s -> output_specified := true; output := s),
254		"output-file Specifiy the resulting LaTeX file";
255		"-n", Arg.Int (fun n -> linelen := n),
256		"line-width Set the line width";
257		"-image", Arg.String (fun s -> image := s),
258		"coq-image Use coq-image as Coq command";
259		"-w", Arg.Set cut_at_blanks,
260		" Try to cut lines at blanks";
261		"-v", Arg.Set verbose,
262		" Verbose mode (show Coq answers on stdout)";
263		"-sl", Arg.Set slanted,
264		" Coq answers in slanted font (only with LaTeX2e)";
265		"-hrule", Arg.Set hrule,
266		" Coq parts are written between 2 horizontal lines";
267		"-small", Arg.Set small,
268		" Coq parts are written in small font"
269		]
270		(fun s -> files := s :: !files)
271		"coq-tex [options] file ..."
272
273		let main () =
274		parse_cl ();
275		if !image = "" then begin
276		Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
277		image := "coqtop"
278		end;
279		if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin
280		Printf.printf "Error: ";
281		let _ = Sys.command (!image ^ " -batch") in
282		exit 1
283		end else begin
284		Printf.printf "Your version of coqtop seems OK\n";
285		flush stdout
286		end;
287		List.iter one_file (List.rev !files)
288
289		let _ = Printexc.catch main ()

+4

-2

tools/coqdep_common.ml less more

287	287	\| (f,_) :: _ -> escape f
288	288	\| _ -> escape f
289	289
290		let traite_fichier_Coq verbose f =
	290	let rec traite_fichier_Coq verbose f =
291	291	try
292	292	let chan = open_in f in
293	293	let buf = Lexing.from_channel chan in

346	346	addQueue deja_vu_v [str];
347	347	try
348	348	let file_str = Hashtbl.find vKnown [str] in
349		printf " %s.v" (canonize file_str)
	349	let canon = canonize file_str in
	350	printf " %s.v" canon;
	351	traite_fichier_Coq true (canon ^ ".v")
350	352	with Not_found -> ()
351	353	end
352	354	\| AddLoadPath _ \| AddRecLoadPath _ -> (* TODO *) ()

+16

-18

tools/coqdoc/index.ml less more

34	34	type index_entry =
35	35	\| Def of string * entry_type
36	36	\| Ref of coq_module * string * entry_type
37		\| Mod of coq_module * string
38	37
39	38	let current_type : entry_type ref = ref Library
40	39	let current_library = ref ""
41	40	(** refers to the file being parsed *)
42	41
43		(** [deftable] stores only definitions and is used to interpolate idents
44		inside comments, which are not globalized otherwise. *)
45
	42	(** [deftable] stores only definitions and is used to build the index *)
46	43	let deftable = Hashtbl.create 97
	44
	45	(** [byidtable] is used to interpolate idents inside comments, which are not
	46	globalized otherwise. *)
	47	let byidtable = Hashtbl.create 97
47	48
48	49	(** [reftable] stores references and definitions *)
49	50	let reftable = Hashtbl.create 97

58	59	else ""
59	60
60	61	let add_def loc1 loc2 ty sp id =
	62	let fullid = full_ident sp id in
	63	let def = Def (fullid, ty) in
61	64	for loc = loc1 to loc2 do
62		Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
	65	Hashtbl.add reftable (!current_library, loc) def
63	66	done;
64		Hashtbl.add deftable id (Def (full_ident sp id, ty))
	67	Hashtbl.add deftable !current_library (fullid, ty);
	68	Hashtbl.add byidtable id (!current_library, fullid, ty)
65	69
66	70	let add_ref m loc m' sp id ty =
	71	let fullid = full_ident sp id in
67	72	if Hashtbl.mem reftable (m, loc) then ()
68		else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
	73	else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty));
69	74	let idx = if id = "<>" then m' else id in
70		if Hashtbl.mem deftable idx then ()
71		else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
72
73		let add_mod m loc m' id =
74		Hashtbl.add reftable (m, loc) (Mod (m', id));
75		Hashtbl.add deftable m (Mod (m', id))
	75	if Hashtbl.mem byidtable idx then ()
	76	else Hashtbl.add byidtable idx (m', fullid, ty)
76	77
77	78	let find m l = Hashtbl.find reftable (m, l)
78	79
79		let find_string m s = Hashtbl.find deftable s
	80	let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
80	81
81	82	(s Manipulating path prefixes )
82	83

288	289	let l = try Hashtbl.find bt t with Not_found -> [] in
289	290	Hashtbl.replace bt t ((s,m) :: l)
290	291	in
291		let classify m e = match e with
292		\| Def (s,t) -> add_g s m t; add_bt t s m
293		\| Ref _ \| Mod _ -> ()
294		in
	292	let classify m (s,t) = (add_g s m t; add_bt t s m) in
295	293	Hashtbl.iter classify deftable;
296	294	Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
297	295	{ idx_name = "global";

+2

-1

tools/coqdoc/index.mli less more

33	33	type index_entry =
34	34	\| Def of string * entry_type
35	35	\| Ref of coq_module * string * entry_type
36		\| Mod of coq_module * string
37	36
	37	(* Find what symbol coqtop said is located at loc in the source file *)
38	38	val find : coq_module -> loc -> index_entry
39	39
	40	(* Find what data is referred to by some string in some coq module *)
40	41	val find_string : coq_module -> string -> index_entry
41	42
42	43	val add_module : coq_module -> unit

+18

-35

tools/coqdoc/output.ml less more

125	125
126	126	let token_tree_texmacs = ref (initialize_texmacs ())
127	127
	128	let token_tree_latex = ref Tokens.empty_ttree
	129	let token_tree_html = ref Tokens.empty_ttree
	130
128	131	let initialize_tex_html () =
129	132	let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
130		List.fold_right (fun (s,l,l') (tt,tt') ->
	133	let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') ->
131	134	(Tokens.ttree_add tt s l,
132	135	match l' with None -> tt' \| Some l' -> Tokens.ttree_add tt' s l'))
133	136	[ "*" , "\\ensuremath{\\times}", if_utf8 "×";

150	153	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
151	154	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
152	155	(* "fun", "\\ensuremath{\\lambda}" ? *)
153		] (Tokens.empty_ttree,Tokens.empty_ttree)
154
155		let token_tree_latex = ref (fst (initialize_tex_html ()))
156		let token_tree_html = ref (snd (initialize_tex_html ()))
	156	] (Tokens.empty_ttree,Tokens.empty_ttree) in
	157	token_tree_latex := tree_latex;
	158	token_tree_html := tree_html
157	159
158	160	let add_printing_token s (t1,t2) =
159	161	(match t1 with None -> () \| Some t1 ->

324	326	let space = 0.5 *. (float n) in
325	327	printf "\\coqdocindent{%2.2fem}\n" space
326	328
327		let module_ref m s =
328		printf "\\coqdocmodule{%s}{%s}" m (escaped s)
329
330	329	let ident_ref m fid typ s =
331	330	let id = if fid <> "" then (m ^ "." ^ fid) else m in
332	331	match find_module m with

355	354	let reference s = function
356	355	\| Def (fullid,typ) ->
357	356	defref (get_module false) fullid typ s
358		\| Mod (m,s') when s = s' ->
359		module_ref m s
360	357	\| Ref (m,fullid,typ) ->
361	358	ident_ref m fullid typ s
362		\| Mod _ ->
363		printf "\\coqdocvar{%s}" (escaped s)
364	359
365	360	(*s The sublexer buffers symbol characters and attached
366	361	uninterpreted ident and try to apply special translation such as,

388	383	last_was_in := false
389	384
390	385	let initialize () =
	386	initialize_tex_html ();
391	387	Tokens.token_tree := token_tree_latex;
392	388	Tokens.outfun := output_sublexer_string
393	389

533	529	end
534	530
535	531	let trailer () =
536		if !index && (get_module false) <> "Index" then
537		printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
538		if !header_trailer then
539		if !footer_file_spec then
	532	if !header_trailer && !footer_file_spec then
540	533	let cin = Pervasives.open_in !footer_file in
541	534	try
542	535	while true do

544	537	printf "%s\n" s
545	538	done
546	539	with End_of_file -> Pervasives.close_in cin
547		else
548		begin
549		printf "<hr/>This page has been generated by ";
550		printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
551		printf "</div>\n\n</div>\n\n</body>\n</html>"
552		end
	540	else
	541	begin
	542	if !index && (get_module false) <> "Index" then
	543	printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
	544	printf "<hr/>This page has been generated by ";
	545	printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
	546	printf "</div>\n\n</div>\n\n</body>\n</html>"
	547	end
553	548
554	549	let start_module () =
555	550	let ln = !lib_name in

619	614	\| Some n -> n
620	615	\| None -> addr)
621	616
622		let module_ref m s =
623		match find_module m with
624		\| Local ->
625		printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
626		\| External m when !externals ->
627		printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
628		\| External _ \| Unknown ->
629		output_string s
630
631	617	let ident_ref m fid typ s =
632	618	match find_module m with
633	619	\| Local ->

644	630	\| Def (fullid,ty) ->
645	631	printf "<a name=\"%s\">" fullid;
646	632	printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
647		\| Mod (m,s') when s = s' ->
648		module_ref m s
649	633	\| Ref (m,fullid,ty) ->
650	634	ident_ref m fullid (type_name ty) s
651		\| Mod _ ->
652		printf "<span class=\"id\" type=\"mod\">%s</span>" s
653	635
654	636	let output_sublexer_string doescape issymbchar tag s =
655	637	let s = if doescape then escaped s else s in

666	648	Tokens.output_tagged_symbol_char tag c
667	649
668	650	let initialize () =
	651	initialize_tex_html();
669	652	Tokens.token_tree := token_tree_html;
670	653	Tokens.outfun := output_sublexer_string
671	654

+1

-1

tools/fake_ide.ml less more

20	20	Xml_utils.print_xml (snd !coqtop) xml_query;
21	21	flush (snd !coqtop);
22	22	let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in
23		let res = Ide_intf.to_answer xml_answer in
	23	let res = Ide_intf.to_answer xml_answer call in
24	24	prerr_endline (Ide_intf.pr_full_value call res);
25	25	match res with Interface.Fail _ -> exit 1 \| _ -> ()
26	26

+93

-63

toplevel/ide_intf.ml less more

44	44	evars : unit -> evar list option;
45	45	hints : unit -> (hint list * hint) option;
46	46	status : unit -> status;
47		search : search_flags -> search_answer list;
	47	search : search_flags -> string coq_object list;
48	48	get_options : unit -> (option_name * option_state) list;
49	49	set_options : (option_name * option_value) list -> unit;
50	50	inloadpath : string -> bool;

62	62	let evars : evar list option call = Evars
63	63	let hints : (hint list * hint) option call = Hints
64	64	let status : status call = Status
65		let search flags : search_answer list call = Search flags
	65	let search flags : string coq_object list call = Search flags
66	66	let get_options : (option_name * option_state) list call = GetOptions
67	67	let set_options l : unit call = SetOptions l
68	68	let inloadpath s : bool call = InLoadPath s

80	80	\| Evars -> Obj.magic (handler.evars () : evar list option)
81	81	\| Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
82	82	\| Status -> Obj.magic (handler.status () : status)
83		\| Search flags -> Obj.magic (handler.search flags : search_answer list)
	83	\| Search flags -> Obj.magic (handler.search flags : string coq_object list)
84	84	\| GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
85	85	\| SetOptions opts -> Obj.magic (handler.set_options opts : unit)
86	86	\| InLoadPath s -> Obj.magic (handler.inloadpath s : bool)

129	129
130	130	(** Base types *)
131	131
	132	let of_unit () = Element ("unit", [], [])
	133
	134	let to_unit = function
	135	\| Element ("unit", [], []) -> ()
	136	\| _ -> raise Marshal_error
	137
132	138	let of_bool b =
133	139	if b then constructor "bool" "true" []
134	140	else constructor "bool" "false" []

165	171	let of_int i = Element ("int", [], [PCData (string_of_int i)])
166	172
167	173	let to_int = function
168		\| Element ("int", [], [PCData s]) -> int_of_string s
	174	\| Element ("int", [], [PCData s]) ->
	175	(try int_of_string s with Failure _ -> raise Marshal_error)
169	176	\| _ -> raise Marshal_error
170	177
171	178	let of_pair f g (x, y) = Element ("pair", [], [f x; g y])

231	238	\| "include_blacklist" -> Include_Blacklist
232	239	\| _ -> raise Marshal_error)
233	240
234		let of_search_answer ans =
235		let path = of_list of_string ans.search_answer_full_path in
236		let name = of_string ans.search_answer_base_name in
237		let tpe = of_string ans.search_answer_type in
238		Element ("search_answer", [], [path; name; tpe])
239
240		let to_search_answer = function
241		\| Element ("search_answer", [], [path; name; tpe]) ->
242		let path = to_list to_string path in
243		let name = to_string name in
244		let tpe = to_string tpe in {
245		search_answer_full_path = path;
246		search_answer_base_name = name;
247		search_answer_type = tpe;
	241	let of_coq_object f ans =
	242	let prefix = of_list of_string ans.coq_object_prefix in
	243	let qualid = of_list of_string ans.coq_object_qualid in
	244	let obj = f ans.coq_object_object in
	245	Element ("coq_object", [], [prefix; qualid; obj])
	246
	247	let to_coq_object f = function
	248	\| Element ("coq_object", [], [prefix; qualid; obj]) ->
	249	let prefix = to_list to_string prefix in
	250	let qualid = to_list to_string qualid in
	251	let obj = f obj in {
	252	coq_object_prefix = prefix;
	253	coq_object_qualid = qualid;
	254	coq_object_object = obj;
248	255	}
249	256	\| _ -> raise Marshal_error
250	257

411	418	}
412	419	\| _ -> raise Marshal_error
413	420
414		let of_hints =
415		let of_hint = of_list (of_pair of_string of_string) in
416		of_option (of_pair (of_list of_hint) of_hint)
417
418		let of_answer (q : 'a call) (r : 'a value) =
419		let convert = match q with
420		\| Interp _ -> Obj.magic (of_string : string -> xml)
421		\| Rewind _ -> Obj.magic (of_int : int -> xml)
422		\| Goal -> Obj.magic (of_option of_goals : goals option -> xml)
423		\| Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml)
424		\| Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml)
425		\| Status -> Obj.magic (of_status : status -> xml)
426		\| Search _ -> Obj.magic (of_list of_search_answer : search_answer list -> xml)
427		\| GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml)
428		\| SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], []))
429		\| InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
430		\| MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
431		\| Quit -> Obj.magic (fun _ -> Element ("unit", [], []))
432		\| About -> Obj.magic (of_coq_info : coq_info -> xml)
433		in
434		of_value convert r
435
436		let to_answer xml =
437		let rec convert elt = match elt with
438		\| Element (tpe, attrs, l) ->
439		begin match tpe with
440		\| "unit" -> Obj.magic ()
441		\| "string" -> Obj.magic (to_string elt : string)
442		\| "int" -> Obj.magic (to_int elt : int)
443		\| "status" -> Obj.magic (to_status elt : status)
444		\| "bool" -> Obj.magic (to_bool elt : bool)
445		\| "list" -> Obj.magic (to_list convert elt : 'a list)
446		\| "option" -> Obj.magic (to_option convert elt : 'a option)
447		\| "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b))
448		\| "goals" -> Obj.magic (to_goals elt : goals)
449		\| "evar" -> Obj.magic (to_evar elt : evar)
450		\| "option_value" -> Obj.magic (to_option_value elt : option_value)
451		\| "option_state" -> Obj.magic (to_option_state elt : option_state)
452		\| "coq_info" -> Obj.magic (to_coq_info elt : coq_info)
453		\| "search_answer" -> Obj.magic (to_search_answer elt : search_answer)
454		\| _ -> raise Marshal_error
455		end
456		\| _ -> raise Marshal_error
457		in
458		to_value convert xml
	421	(** Conversions between ['a value] and xml answers
	422
	423	When decoding an xml answer, we dynamically check that it is compatible
	424	with the original call. For that we now rely on the fact that all
	425	sub-fonctions [to_xxx : xml -> xxx] check that the current xml element
	426	is "xxx", and raise [Marshal_error] if anything goes wrong.
	427	*)
	428
	429	type value_type =
	430	\| Unit \| String \| Int \| Bool \| Goals \| Evar \| State \| Option_state \| Coq_info
	431	\| Option of value_type
	432	\| List of value_type
	433	\| Coq_object of value_type
	434	\| Pair of value_type * value_type
	435
	436	let hint = List (Pair (String, String))
	437	let option_name = List String
	438
	439	let expected_answer_type = function
	440	\| Interp _ -> String
	441	\| Rewind _ -> Int
	442	\| Goal -> Option Goals
	443	\| Evars -> Option (List Evar)
	444	\| Hints -> Option (Pair (List hint, hint))
	445	\| Status -> State
	446	\| Search _ -> List (Coq_object String)
	447	\| GetOptions -> List (Pair (option_name, Option_state))
	448	\| SetOptions _ -> Unit
	449	\| InLoadPath _ -> Bool
	450	\| MkCases _ -> List (List String)
	451	\| Quit -> Unit
	452	\| About -> Coq_info
	453
	454	let of_answer (q : 'a call) (r : 'a value) : xml =
	455	let rec convert ty : 'a -> xml = match ty with
	456	\| Unit -> Obj.magic of_unit
	457	\| Bool -> Obj.magic of_bool
	458	\| String -> Obj.magic of_string
	459	\| Int -> Obj.magic of_int
	460	\| State -> Obj.magic of_status
	461	\| Option_state -> Obj.magic of_option_state
	462	\| Coq_info -> Obj.magic of_coq_info
	463	\| Goals -> Obj.magic of_goals
	464	\| Evar -> Obj.magic of_evar
	465	\| List t -> Obj.magic (of_list (convert t))
	466	\| Option t -> Obj.magic (of_option (convert t))
	467	\| Coq_object t -> Obj.magic (of_coq_object (convert t))
	468	\| Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2))
	469	in
	470	of_value (convert (expected_answer_type q)) r
	471
	472	let to_answer xml (c : 'a call) : 'a value =
	473	let rec convert ty : xml -> 'a = match ty with
	474	\| Unit -> Obj.magic to_unit
	475	\| Bool -> Obj.magic to_bool
	476	\| String -> Obj.magic to_string
	477	\| Int -> Obj.magic to_int
	478	\| State -> Obj.magic to_status
	479	\| Option_state -> Obj.magic to_option_state
	480	\| Coq_info -> Obj.magic to_coq_info
	481	\| Goals -> Obj.magic to_goals
	482	\| Evar -> Obj.magic to_evar
	483	\| List t -> Obj.magic (to_list (convert t))
	484	\| Option t -> Obj.magic (to_option (convert t))
	485	\| Coq_object t -> Obj.magic (to_coq_object (convert t))
	486	\| Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2))
	487	in
	488	to_value (convert (expected_answer_type c)) xml
459	489
460	490	(** * Debug printing *)
461	491

+2

-2

toplevel/ide_intf.mli less more

76	76	evars : unit -> evar list option;
77	77	hints : unit -> (hint list * hint) option;
78	78	status : unit -> status;
79		search : search_flags -> search_answer list;
	79	search : search_flags -> string coq_object list;
80	80	get_options : unit -> (option_name * option_state) list;
81	81	set_options : (option_name * option_value) list -> unit;
82	82	inloadpath : string -> bool;

103	103	val to_call : xml -> 'a call
104	104
105	105	val of_answer : 'a call -> 'a value -> xml
106		val to_answer : xml -> 'a value
	106	val to_answer : xml -> 'a call -> 'a value
107	107
108	108	(** * Debug printing *)
109	109

+36

-23

toplevel/ide_slave.ml less more

126	126	let id_s = Names.string_of_id id in
127	127	let type_s = string_of_ppcmds (pr_ltype_env env ast) in
128	128	[
129		("clear "^id_s),("clear "^id_s^".\n");
130		("apply "^id_s),("apply "^id_s^".\n");
131		("exact "^id_s),("exact "^id_s^".\n");
132		("generalize "^id_s),("generalize "^id_s^".\n");
133		("absurd <"^id_s^">"),("absurd "^type_s^".\n")
	129	("clear "^id_s),("clear "^id_s^".");
	130	("apply "^id_s),("apply "^id_s^".");
	131	("exact "^id_s),("exact "^id_s^".");
	132	("generalize "^id_s),("generalize "^id_s^".");
	133	("absurd <"^id_s^">"),("absurd "^type_s^".")
134	134	] @ [
135		("discriminate "^id_s),("discriminate "^id_s^".\n");
136		("injection "^id_s),("injection "^id_s^".\n")
	135	("discriminate "^id_s),("discriminate "^id_s^".");
	136	("injection "^id_s),("injection "^id_s^".")
137	137	] @ [
138		("rewrite "^id_s),("rewrite "^id_s^".\n");
139		("rewrite <- "^id_s),("rewrite <- "^id_s^".\n")
	138	("rewrite "^id_s),("rewrite "^id_s^".");
	139	("rewrite <- "^id_s),("rewrite <- "^id_s^".")
140	140	] @ [
141		("elim "^id_s), ("elim "^id_s^".\n");
142		("inversion "^id_s), ("inversion "^id_s^".\n");
143		("inversion clear "^id_s), ("inversion_clear "^id_s^".\n")
	141	("elim "^id_s), ("elim "^id_s^".");
	142	("inversion "^id_s), ("inversion "^id_s^".");
	143	("inversion clear "^id_s), ("inversion_clear "^id_s^".")
144	144	]
145	145
146	146	let concl_next_tac sigma concl =
147		let expand s = (s,s^".\n") in
	147	let expand s = (s,s^".") in
148	148	List.map expand ([
149	149	"intro";
150	150	"intros";

311	311	in
312	312	let ans = ref [] in
313	313	let print_function ref env constr =
314		let name = Names.string_of_id (Nametab.basename_of_global ref) in
315		let make_path = Names.string_of_id in
316		let path =
317		List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref))
318		in
319		let answer = {
320		Interface.search_answer_full_path = path;
321		Interface.search_answer_base_name = name;
322		Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr);
323		} in
	314	let fullpath = repr_dirpath (Nametab.dirpath_of_global ref) in
	315	let qualid = Nametab.shortest_qualid_of_global Idset.empty ref in
	316	let (shortpath, basename) = Libnames.repr_qualid qualid in
	317	let shortpath = repr_dirpath shortpath in
	318	(* [shortpath] is a suffix of [fullpath] and we're looking for the missing
	319	prefix *)
	320	let rec prefix full short accu = match full, short with
	321	\| _, [] ->
	322	let full = List.rev_map string_of_id full in
	323	(full, accu)
	324	\| _ :: full, m :: short ->
	325	prefix full short (string_of_id m :: accu)
	326	\| _ -> assert false
	327	in
	328	let (prefix, qualid) = prefix fullpath shortpath [string_of_id basename] in
	329	let answer = {
	330	Interface.coq_object_prefix = prefix;
	331	Interface.coq_object_qualid = qualid;
	332	Interface.coq_object_object = string_of_ppcmds (pr_lconstr_env env constr);
	333	} in
324	334	ans := answer :: !ans;
325	335	in
326	336	let () = Search.gen_filtered_search filter_function print_function in

431	441	let () = pr_debug ("--> " ^ Ide_intf.pr_full_value q r) in
432	442	Ide_intf.of_answer q r
433	443	with
	444	\| Xml_parser.Error (Xml_parser.Empty, _) ->
	445	pr_debug ("End of input, exiting");
	446	exit 0
434	447	\| Xml_parser.Error (err, loc) ->
435	448	let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in
436	449	fail msg

+8

-4

toplevel/interface.mli less more

85	85	the flag should be negated. *)
86	86	type search_flags = (search_constraint * bool) list
87	87
88		type search_answer = {
89		search_answer_full_path : string list;
90		search_answer_base_name : string;
91		search_answer_type : string;
	88	(** A named object in Coq. [coq_object_qualid] is the shortest path defined for
	89	the user. [coq_object_prefix] is the missing part to recover the fully
	90	qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid].
	91	[coq_object_object] is the actual content of the object. *)
	92	type 'a coq_object = {
	93	coq_object_prefix : string list;
	94	coq_object_qualid : string list;
	95	coq_object_object : 'a;
92	96	}
93	97
94	98	type coq_info = {

+1

-1

toplevel/vernacentries.ml less more

207	207	str "\| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
208	208	in
209	209	msg (v 1 (str "match # with" ++ fnl () ++
210		prlist_with_sep fnl pr_branch patterns ++ fnl ()))
	210	prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ()))
211	211
212	212	(* "Print" commands *)
213	213