coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Extraction: only do the test on generalizable lets for ocaml	letouzey	2011-12-10
*	Extraction: avoid internal eta-reduction (fix #2570)	letouzey	2011-12-08
*	Extraction: try to avoid issues with an Include directly inside a .v	letouzey	2011-11-30
*	Extraction: Richer patterns in matchs as proposed by P.N. Tollitte	letouzey	2011-11-28
*	Extraction Implicit: fix the numbering of constructor arguments	letouzey	2011-09-05
*	Extraction: allow extraction of records with anonymous fields (fix #2555)	letouzey	2011-08-25
*	Extraction: replace generic = on mutual_inductive_body by mib_equal	puech	2011-07-29
*	Set Extraction KeepSingleton: an option for not decapsulating singleton types	letouzey	2011-07-04
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Extraction: opaque terms are not traversed anymore by default	letouzey	2011-04-13
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Extraction: customized inductives are always standard	glondu	2011-03-31
*	Extraction: a warning when an opaque constant is enterred	letouzey	2011-03-07
*	Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)	letouzey	2010-12-21
*	Dead code in extraction	letouzey	2010-09-24
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extraction: more factorization of common match branches	letouzey	2010-07-08
*	Extraction with implicits: perform the occur-check after optimisations	letouzey	2010-06-08
*	Extraction: fix type_expunge_from_sign broken in last commit	letouzey	2010-05-01
*	Extraction: an experimental command to get rid of some cst/constructor arguments	letouzey	2010-04-30
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Extraction: less eta in calls to global functions, better optimization phase	letouzey	2010-04-16
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Extraction: ad-hoc identifier type with annotations for reductions	letouzey	2010-04-16
*	Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-e...	letouzey	2010-04-16
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20