coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Changing the type of Ltac values. Now they are toplevel generic	ppedrot	2013-06-12
*	Moved Stringset and Stringmap to String namespace.	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Added a CString module.	ppedrot	2012-11-13
*	More cleanup of Util: utf8 aspects moved to a new file unicode.ml	letouzey	2012-09-18
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Added some tricky tail-rec versions of List functions to CList	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Revert copy/pasted function in to minilib thanks to clib.cma	pboutill	2012-05-23
*	Adding newline after warning and restoring distinction between	herbelin	2012-04-15
*	Unification: Added a heuristic to solve problems of the form	herbelin	2012-03-26
*	Reorganizing the structure of evarutil.ml (only restructuration, no	herbelin	2012-03-20
*	Yet another subtlety with bug 2732: when several grammar rules of a	herbelin	2012-03-18
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Added ability to take the type of applied metas into account when	herbelin	2011-12-17
*	Finally used typing to decide whether an alias needs to be expanded or	herbelin	2011-11-28
*	Added list_map_filter_i	msozeau	2011-08-10
*	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-07-29
*	More work on error handling	letouzey	2011-05-17
*	Starting being more explicit on the reasons why module subtyping fails.	herbelin	2011-03-05
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin	2010-07-29
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin	2010-07-22
*	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau	2010-06-30
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Extraction: replace unicode characters in ident by ascii encodings (fix #2158...	letouzey	2010-06-21
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Nicer representation of tokens, more independant of camlp*	letouzey	2010-05-19
*	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-29
*	Added a new exception for already declared Schemes,	vsiles	2010-04-27
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	Experiment propagation of implicit arguments and arguments scope for	herbelin	2009-11-12
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin	2009-09-26
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17