coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-04	Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...	letouzey
2010-03-04	Makefile: make devdocclean was not removing .dep.ps, btw let's remove .dep....	letouzey
2010-01-28	Remove bashisms	glondu
2010-01-12	Added module sharing support for typeclasses and hints (pri_auto_tactic).	soubiran
2010-01-08	* Segmenttree: New. A very simple implementation of segment trees.	regisgia
2010-01-04	Few misc. updates.	herbelin
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-20	* Rewrite [classify_unicode] using standard unicode tables.	regisgia
2009-12-13	Addition of mergesort + cleaning of the Sorting library	herbelin
2009-12-02	Remove interface plugin	glondu
2009-11-13	Remove useless ppevd (which is identical to ppevm)	glondu
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Fixed bug #2168 (closing a section may have as side-effect the erasure	herbelin
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-08	Fixed "Scheme Equality" when another instance of the scheme on the	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-08	Fixed clash names in Relations (see bug report #2152) and make names	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-14	Mise à jour du document de révision de la stdlib et déplacement de la	herbelin
2009-08-07	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-05-26	ocamldebug-coq: add some forgotten -I	letouzey
2009-05-24	Moved and completed the history of Coq versions from the	herbelin
2009-05-20	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-04-25	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin
2009-04-14	Correction du patch -rectypes pour ocaml 3.10	vsiles
2009-03-31	Complementary fix to have ocamlopt_shared_os5fix.sh working correctly	herbelin
2009-03-30	Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)	letouzey
2009-03-29	ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)	letouzey
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-03-17	Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2009-02-17	#rectypes was already automatically added when using 3.11	herbelin
2009-02-17	Made hack to have Drop and #use"include" working with ocaml 3.10 public	herbelin
2009-02-11	Document how FIND_VCS_CLAUSE has to be used	lmamane
2009-01-19	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin
2009-01-05	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-09	About "apply in":	herbelin
2008-11-19	Execute #rectypes directive in embedded OCaml toplevel...	glondu
2008-11-07	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin