coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Extraction: allow to use Extraction Inline / NoInline even from under a section.	letouzey	2010-10-06
*	Remove unused unshare_proof_tree from xml plugin	glondu	2010-10-06
*	Remove open_subgoals field of proof_tree	glondu	2010-10-06
*	Auto-inlining of f_terminate in Function	jforest	2010-10-05
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Remove "init" label from Termops.it_mk* specialized functions	glondu	2010-09-28
*	Dead code in extraction	letouzey	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Report fix bug 2345 from v8.3 (Bad error message when functional	courtieu	2010-09-21
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	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
*	Extraction: multiple fixes related with the Not_found encountered by X. Leroy	letouzey	2010-09-17
*	Fix likely semantic typos	glondu	2010-09-15
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	commit 13400 and 13409.	soubiran	2010-09-13
*	fixed bug #2375 (congruence)	corbinea	2010-09-02
*	Fix [clenv_missing] to compute a better approximation of missing	msozeau	2010-08-02
*	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier	2010-07-28
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...	pottier	2010-07-28