coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Call process_vernac_interp_error before calling Errors.print in	herbelin	2011-06-10
*	Revert "Check if recursive calls are guarded before printing "Proof completed"."	pboutill	2011-06-10
*	ring2, cring, nsatz avec type classe avec parametres plus notations	pottier	2011-06-10
*	Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...	msozeau	2011-06-07
*	Fix bug #2415: warn when closing modules or sections and some obligations are...	msozeau	2011-06-07
*	Check if recursive calls are guarded before printing "Proof completed".	herbelin	2011-05-26
*	Q2R -> IQR	fbesson	2011-05-25
*	Made the emacs-U option deprecated. Also removed the old code	courtieu	2011-05-24
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...	fbesson	2011-05-23
*	added support to handle division by a constant over R	fbesson	2011-05-20
*	Extraction: avoid lots of late mind_of_kn	letouzey	2011-05-19
*	Extraction: global reference should be indexed on their user part (fix #2540)	letouzey	2011-05-19
*	cbv delta - [...] before calling lia	fbesson	2011-05-18
*	apply zeta reduction before syntaxification	fbesson	2011-05-18
*	Extraction: avoid printing of Recursive Extraction in coqide's console	letouzey	2011-05-18
*	Fixed my last patch: these files no longer use nat_beq (automatically	vsiles	2011-05-16
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Improved lia + experimental nlia	fbesson	2011-05-09
*	Additionnal fix of romega after modularisation of ZArith	letouzey	2011-05-06
*	Modularisation of Znat, a few name changed elsewhere	letouzey	2011-05-05
*	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 BinNat + fixes of stdlib	letouzey	2011-05-05
*	Modularization of Pnat	letouzey	2011-05-05
*	Modularization of BinPos + fixes in Stdlib	letouzey	2011-05-05
*	Definitions of positive, N, Z moved in Numbers/BinNums.v	letouzey	2011-05-05
*	Extraction: allow extraction foo when foo is an alias notation	letouzey	2011-05-05
*	First phase removing obsolete support for eta up to conversion in	herbelin	2011-05-04
*	Fixed a bug causing inconsistent states during proof editting.	aspiwack	2011-04-29
*	bug fix: concurrent access of persistent_cache	fbesson	2011-04-21
*	Declarative mode: fix escape and return.	aspiwack	2011-04-19
*	Extraction: nicer error when a toplevel module has no body (#2525)	letouzey	2011-04-15
*	Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)	letouzey	2011-04-15
*	Extraction: opaque terms are not traversed anymore by default	letouzey	2011-04-13
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	Extraction: unfolds the let-in created by Program when handling "match"	letouzey	2011-04-07
*	Extraction: avoid some useless Obj.magic by fixing my ML type unifier	letouzey	2011-04-07
*	Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.	aspiwack	2011-04-06
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Quickly avoid global axioms in Loic new files about ring	letouzey	2011-04-03
*	Extraction: customized inductives are always standard	glondu	2011-03-31
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Keep information on which fields are subclasses in class declarations,	msozeau	2011-03-11
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	syntax for exponents	pottier	2011-03-08