coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-28	ZArith/Int: no need to load romega here (but rather in FullAVL)	letouzey
2009-03-28	ZMicromega: useless dependency toward ZArith.Int	letouzey
2009-03-27	Coqdep: some dead code and code move (first experiment with Oug)	letouzey
2009-03-27	Parsing files for numerals (+ ascii/string) moved into plugins	letouzey
2009-03-27	Remove unused mli files	letouzey
2009-03-27	GroebnerZ: no more admitted lemmas	letouzey
2009-03-26	Ocamlbuild: 1st reasonably complete version (rules for binaries + plugins + vo)	letouzey
2009-03-26	Fixes in Program well-founded definitions:	msozeau
2009-03-26	ocamlbuild: coqide, coqchk, a bit of .vo	letouzey
2009-03-26	Coqdep_boot: one line with bad indentation	letouzey
2009-03-26	Protect typeset arguments in titles in LaTeX output (fixes compilation	msozeau
2009-03-26	clean revision and coqdep_boot, too	lmamane
2009-03-26	bin/coq-{parser,interface}: use this coqtop, not the first in $PATH	lmamane
2009-03-25	make coqdep_boot in stage1, not stage2	lmamane
2009-03-24	Fix coqdoc bugs reported by Ian Lynagh.	msozeau
2009-03-24	ocamlbuild improvements + minor makefile fix	letouzey
2009-03-24	pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)	letouzey
2009-03-23	- Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"	herbelin
2009-03-22	Backport from v8.2 branch of 11986 (interpretation of quantified	herbelin
2009-03-22	Compromise wrt introduction-names compatibility issue after addition	herbelin
2009-03-22	More elaborate handling of newlines in Gallina mode. Support inline	msozeau
2009-03-22	coqdoc fixes and support for parsing regular comments (request by	msozeau
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-20	Makefile: avoid $(ML4FILES:.ml4=.ml) since this is $(ML4FILESML)	letouzey
2009-03-20	replaced dir_load by load_file because dir_load does not raise an exception w...	barras
2009-03-20	delete contrib dirs	barras
2009-03-20	Fixes to make Ynot compile with the trunk:	msozeau
2009-03-20	Compatibility with Apple's non-gnu sed.	msozeau
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-03-19	coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...	barras
2009-03-18	renamed %-mod.ml into %_mod.ml to avoid ocaml warning	barras
2009-03-18	fixed ring/field warning about hyp cleaning up	barras
2009-03-18	removed correctness dirs	barras
2009-03-18	coq_makefile: no ml dependency on coq sources	barras
2009-03-17	Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)	herbelin
2009-03-17	- gros commit sur ring et field: passage des arguments simplifie	barras
2009-03-17	Makefile:clean: rm *-mod.ml	barras
2009-03-17	- configure: affiche si le natdynlink est positionne	barras
2009-03-16	missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was includ...	barras
2009-03-16	coqdep_boot: a specialized and dependency-free coqdep for killing one of the ...	letouzey
2009-03-16	Makefile: fix ignored errors, several attempts to clarify things	letouzey
2009-03-16	Makefile: minor improvements	letouzey
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-03-14	Better mechanism for loading initial plugins	letouzey
2009-03-14	RefMan: a label defined twice	letouzey
2009-03-14	Makefile: ml dependencies of contribs are moved to .mllib files	letouzey
2009-03-14	Coqdep: better handling of Declare ML Module (via .mllib) + many cleanups	letouzey
2009-03-14	Coqdep: remove references to obsolete .zi and Require Implementation stuff	letouzey
2009-03-11	Cleanup: avoid the warning about Coq-tex not being a valid Ocaml module name	letouzey