coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-02	Noise for nothing	pboutill
2011-12-17	Added ability to take the type of applied metas into account when	herbelin
2011-11-28	Finally used typing to decide whether an alias needs to be expanded or	herbelin
2011-08-10	Added list_map_filter_i	msozeau
2011-07-29	Refl_omega: replaced some generic = on constr by eq_constr	puech
2011-07-29	Coq_omega: replaced generic = on constr by eq_constr	puech
2011-07-29	Evarutil: generic equality on constr replaced by eq_constr (x2)	puech
2011-07-29	Tactics: generic equality on constr replaced by eq_constr	puech
2011-05-17	More work on error handling	letouzey
2011-03-05	Starting being more explicit on the reasons why module subtyping fails.	herbelin
2011-02-14	- Fix treatment of globality flag for typeclass instance hints (they	msozeau
2010-10-03	Added multiple implicit arguments rules per name.	herbelin
2010-07-29	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin
2010-06-30	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-21	Extraction: replace unicode characters in ident by ascii encodings (fix #2158...	letouzey
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-08	Fix treatment of {struct x} annotations in presence of generalized	msozeau
2010-05-19	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey
2010-05-19	Nicer representation of tokens, more independant of camlp*	letouzey
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2010-04-27	Added a new exception for already declared Schemes,	vsiles
2010-04-19	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin
2010-04-16	Util: remove list_split_at which is a clone of list_chop	letouzey
2010-02-10	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau
2009-11-12	Experiment propagation of implicit arguments and arguments scope for	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-09-26	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-16	comparison functions on lists and arrays	barras
2009-03-04	Timeout message was not always displayed	barras
2009-03-02	Heavy modifications on the widget and edition tab creation mechanism.	vgross
2009-02-09	memoized is_ground_env	barras
2009-01-23	Petit nettoyage faisant suite au commit #11847 .	aspiwack
2009-01-08	Remove trailing newlines in outputs of X -where	glondu
2009-01-02	Made the debugger work again:	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-22	Affichage des notations récursives:	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-24	Suite commit 11236	notin
2008-07-16	Quelques modifications autour du filtrage Ltac:	herbelin