coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Everything compiles again.	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Proof using ...	gareuselesinge	2011-12-12
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Fix bug #2557 and an issue with Propers for complement	msozeau	2011-10-07
*	Keep obligation source information in Program	msozeau	2011-06-30
*	Merge branch 'subclasses' into coq-trunk	msozeau	2011-05-05
*	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau	2011-04-18
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	- Make typeclass transparency information directly available	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...	msozeau	2011-03-23
*	- 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
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	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
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Fix bug# 2392	msozeau	2010-10-07
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Remove some occurrences of "open Termops"	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	* removed declare_constant and declare_internal_constant	vsiles	2010-09-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Correct wrong handling of evars in instance definitions that prevented	msozeau	2010-06-29
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Fix bug #2245, incorrect handling of Context in sections inside module	msozeau	2010-04-27
*	Specific syntax for Instances in Module Type: Declare Instance	letouzey	2010-01-04
*	Fix bug in last commit, missing a substitution call.	msozeau	2010-01-02
*	Fix handling of instance declarations in presence of let-ins (bug	msozeau	2010-01-01
*	Fix "Existing Instance" to handle globality information and "Existing	msozeau	2009-12-27
*	Fix [Instance: forall ..., C args := t] declarations to behave as	msozeau	2009-11-15
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau	2009-10-09
*	Correctly do backtracking during type class resolution even if only new	msozeau	2009-10-05