coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Updating headers.	herbelin	2012-08-08
*	Getting rid of the undocumented [complete] tactic, which was	ppedrot	2012-07-19
*	Ring_polynom : a restricted simpl instead of a unfold;fold	letouzey	2012-07-07
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	rewrite_db : a first attempt at using rewrite_strat for a quicker autorewrite	letouzey	2012-07-05
*	More cleanup in Ring_polynom and EnvRing	letouzey	2012-07-05
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Everything compiles again.	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Proof using ...	gareuselesinge	2011-12-12
*	Fixing bug #2640 and variants of it (inconsistency between when and	herbelin	2011-11-17
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	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