coq - The formal proof system

Age	Commit message (Expand)	Author
2011-09-19	Makefile.doc: typo, index_url.txt should be index_urls.txt	letouzey
2011-09-19	Fix test-suite/ide for repository compiled without -local (fix #2600)	letouzey
2011-09-18	avoid dependency nightmare by creating coqdep_{lexer,common}.mli	letouzey
2011-09-17	doc/refman/Extraction.tex: no need to actually build euclid.ml	letouzey
2011-09-17	Euclid: make the proof transparent (example of extraction in stdlib)	letouzey
2011-09-17	Various fixes in the Makefiles	letouzey
2011-09-16	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey
2011-09-15	Omega aware of Z.pred (fix #1912)	letouzey
2011-09-15	Re-allowing assumptions during proofs seems safe now (fix #2411)	letouzey
2011-09-15	coqc: Recognize option -force-load-proofs.	letouzey
2011-09-15	Names.make_mbid and co : convert from/to identifier (avoid some String.copy)	letouzey
2011-09-12	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack
2011-09-09	correction du bug 2047	jforest
2011-09-08	More twicks on hash-consing	letouzey
2011-09-07	Fix the hconsing of universes	letouzey
2011-09-06	make world now builds fake_ide (to please coq-bench)	letouzey
2011-09-06	Improved ltac code for zify (fix #2575).	letouzey
2011-09-06	test-suite/ide: misc improvement	letouzey
2011-09-06	Avoid registering λ and Π as keywords just for some private Local Notation	letouzey
2011-09-06	ide/preferences.ml: apparently no `META in Gdk.Tags.modifier	letouzey
2011-09-06	Ocamlbuild : build of fake_ide	letouzey
2011-09-05	fake_ide: a short program to mimic an ide talking to coqtop -ideslave	letouzey
2011-09-05	Coqide: new backtracking code, based on the Backtrack command	letouzey
2011-09-05	Ide_intf: slight reorganisation of the IDE api	letouzey
2011-09-05	Lib: remove strange code about backtracking to the current state	letouzey
2011-09-05	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey
2011-09-05	Remove code concerning the obsolete Set/Unset Undo	letouzey
2011-09-05	Util.error now creates UserError(_,msg) instead of UserError(str,str)	letouzey
2011-09-05	Extraction Implicit: fix the numbering of constructor arguments	letouzey
2011-09-04	Having added a special Cast for remembering the use of conversion	herbelin
2011-09-03	Bug 3596: ocamlbuild: coq_makefile now requires Unix	pboutill
2011-09-02	Bug 2589: Documentation patch of Hendrik Tews	pboutill
2011-09-02	Coq_makefile: bugfix in install rule	pboutill
2011-09-01	Automatic search of project file	pboutill
2011-09-01	Coq_makefile : bug when a project file is not in the current directory.	pboutill
2011-09-01	safe_prerr_endline in Minilib	pboutill
2011-09-01	Add option -f to coqide	pboutill
2011-09-01	Add preferences to say how to deal with a project file.	pboutill
2011-09-01	same_file in Minilib	pboutill
2011-09-01	load_file takes advantage of same_file optimisation	pboutill
2011-09-01	create_session takes the filename as argument.	pboutill
2011-09-01	No more parser for reading coqide pref file	pboutill
2011-09-01	[/]+ is equivalent to [/] in System and its copy	pboutill
2011-09-01	Coq_makefile.absolute_dir -> Minilib.canonical_path_name	pboutill
2011-09-01	Creation of ide/project_file.ml4	pboutill
2011-09-01	gitignore update	pboutill
2011-09-01	Coq_makefile: Bug fix of check_dep	pboutill
2011-09-01	Coq_makefile: process_cmd_line is purely functional.	pboutill
2011-09-01	Coq_makefile: No other function than split_arguments uses a target type.	pboutill
2011-09-01	Coq_makefile: New option -arg to specify a compiler option.	pboutill