coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	moins de reification inutile, noatations standards	pottier	2011-08-04
*	Newring: generic = on constr replaced by eq_constr	puech	2011-07-29
*	replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Newring: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Newring: replaced generic = on constr by eq_constr	puech	2011-07-29
*	Newring: generic Pervasives.compare on constr replaced by constr_ord	puech	2011-07-29
*	Newring: generic equality on constr replaced by constr_equal	puech	2011-07-29
*	Integral domains	pottier	2011-07-26
*	Ring2 devient Ncring et la reification par les type classes est partagee	pottier	2011-07-26
*	Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def	letouzey	2011-06-28
*	Follow-up concerning eqb / ltb / leb comparisons	letouzey	2011-06-21
*	ring2, cring, nsatz avec type classe avec parametres plus notations	pottier	2011-06-10
*	BinInt: Z.add become the alternative Z.add'	letouzey	2011-05-05
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	Setoid_ring: some cleanups related with BinPos and BinNat	letouzey	2011-05-05
*	Modularization of BinPos + fixes in Stdlib	letouzey	2011-05-05
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Quickly avoid global axioms in Loic new files about ring	letouzey	2011-04-03
*	syntax for exponents	pottier	2011-03-08
*	Revert "syntax for exponents"	glondu	2011-02-25
*	syntax for exponents	pottier	2011-02-22
*	anneaux commutatifs ou non, reification sans ml	pottier	2011-02-22
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Integer division: quot and rem (trunc convention) in addition to div and mod	letouzey	2010-11-10
*	Still some more Cpow in Type rather than Set (cf. r13542)	letouzey	2010-10-21
*	Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)	letouzey	2010-10-14
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Reverting partial fix for #2335 committed by mistake in r13435. Sorry.	herbelin	2010-09-19
*	Patch solving the bug but leaving open design choices	herbelin	2010-09-19
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin	2010-07-18
*	Tentative de suppression de l'import automatique des hints et coercions.	herbelin	2010-07-18
*	fixed bug #2316 (ring_simplify)	barras	2010-07-16
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Improvements in generalized rewriting:	msozeau	2010-03-05
*	bug in field_simplify_eq in	barras	2010-02-10
*	Euclidean division for NArith	letouzey	2010-02-10
*	New command Declare Reduction <id> := <conv_expr>.	letouzey	2010-01-28
*	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
*	This big commit addresses two problems:	soubiran	2009-10-21