coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	Extraction: a warning when an opaque constant is enterred	letouzey	2011-03-07
*	Extraction: fix printing of haskell modular names	letouzey	2011-03-07
*	Extraction: avoid printing unused mutual fix components (fix #2477)	letouzey	2011-03-07
*	A new command "Separate Extraction"	letouzey	2011-03-07
*	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin	2011-03-05
*	Extraction: improved indentation of extracted code (fix #2497)	letouzey	2011-03-04
*	Add a flag to hide obligations in Program-generated terms under an	msozeau	2011-02-28
*	Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)	letouzey	2011-02-25
*	Fix indentation of default pattern in haskell case (bug #2476)	letouzey	2011-02-25
*	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
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	Started to fix the declarative proof mode (C-zar).	aspiwack	2011-02-10
*	Dp: another fix suggested by Virgile Prevosto	letouzey	2011-02-03
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)	letouzey	2011-01-07
*	ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED	glondu	2010-12-25
*	Rename mkR* smart constructors (mostly in funind)	glondu	2010-12-25
*	s/raw/glob/g in decl_interp.ml for more consistency	glondu	2010-12-24
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename files in funind to respect new conventions	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Prepare change of nomenclature rawconstr -> glob_constr	glondu	2010-12-23
*	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey	2010-12-21
*	Remove an unused function with a Evd.fold in subtac	letouzey	2010-12-13
*	Dp: minor fix suggested by Virgile Prevosto	letouzey	2010-11-25
*	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
*	Integer division: quot and rem (trunc convention) in addition to div and mod	letouzey	2010-11-10
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Add information of localisation when an error involving an "implicit	herbelin	2010-11-07
*	Move stuff about positive into a distinct PArith subdir	letouzey	2010-11-02
*	An experimental support for open constrs in hints and in "using"	herbelin	2010-10-31
*	Cleaning the use of parentheses around evd and evdref (cosmetic commit).	herbelin	2010-10-31
*	Solve name conflict about pow introduced by commit 13546.	letouzey	2010-10-21
*	Still some more Cpow in Type rather than Set (cf. r13542)	letouzey	2010-10-21
*	Reparation du parseur/printer de nombres BigN	letouzey	2010-10-14
*	Ring : Cpow in Type rather than Set (type of power coeffs in power_theory)	letouzey	2010-10-14
*	Fix bug #2393: allow let-ins inside telescopes (only fails when there's	msozeau	2010-10-12
*	Fix bug# 2392	msozeau	2010-10-07