coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Fixed some missing options from previous commit.	ppedrot	2011-11-24
*	Omega: for non-arithmetical goals, try proving False from context (wish #2236)	letouzey	2011-09-16
*	Omega aware of Z.pred (fix #1912)	letouzey	2011-09-15
*	Improved ltac code for zify (fix #2575).	letouzey	2011-09-06
*	Coq_omega: replaced generic = on constr by eq_constr	puech	2011-07-29
*	Coq_omega: replaced many generic = on constr by eq_constr	puech	2011-07-29
*	Modularisation of Znat, a few name changed elsewhere	letouzey	2011-05-05
*	Modularization of Pnat	letouzey	2011-05-05
*	Modularization of BinPos + fixes in Stdlib	letouzey	2011-05-05
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits	letouzey	2010-11-18
*	Use full path for unknown stuff in omega	glondu	2010-11-16
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey	2009-12-09
*	OrderedType implementation for various numerical datatypes + min/max structures	letouzey	2009-11-03
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	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-20