coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Set Extraction KeepSingleton: an option for not decapsulating singleton types	letouzey	2011-07-04
*	Extraction: in haskell, __ may have any type, no need to unsafeCoerce it	letouzey	2011-07-04
*	Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)	letouzey	2011-07-04
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Fix compilation error	msozeau	2011-06-30
*	Keep obligation source information in Program	msozeau	2011-06-30
*	update of Micromega doc	fbesson	2011-06-29
*	Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def	letouzey	2011-06-28
*	improved tactic names	fbesson	2011-06-28
*	Numbers: a particular case of div_unique	letouzey	2011-06-24
*	Follow-up concerning eqb / ltb / leb comparisons	letouzey	2011-06-21
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Relaxed the constraint introduced in r14190 that froze the existing	herbelin	2011-06-18
*	Fix bug 2269, program typechecker not used in Instance conclusions	msozeau	2011-06-17
*	Tests de nsatz avec la geometrie	pottier	2011-06-16
*	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