coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot	2013-09-05
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	Added printing of instance priority to the Print Instances command.	ppedrot	2013-08-01
*	One more fix for rewrite: disallow resolving of the (partial) constraints	msozeau	2013-06-12
*	Delayed the computation of parameters in sort polymorphism of	herbelin	2013-05-14
*	Replacing compatibility layer for Fmap in Typeclasses. Code was	ppedrot	2013-05-14
*	More semantical-friendly function.	ppedrot	2013-05-14
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau	2013-04-18
*	Fix for bug #3017: wrong handling of the unresolvability status	msozeau	2013-04-03
*	Fix bug# 2994, 2971 about better error messages.	msozeau	2013-03-22
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Allowing different types of, not to be mixed, generic Stores through	ppedrot	2013-03-12
*	Modulification of name	ppedrot	2012-12-18
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Forward-port fixes from 8.4 (15358, 15353, 15333).	msozeau	2012-06-04
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	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
*	Noise for nothing	pboutill	2012-03-02
*	Fix for Program Instance not separately checking the resolution of evars of t...	msozeau	2012-01-23
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Fix for subclasses implementation, allowing to register generalized classes s...	msozeau	2011-11-18
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Fix bug #2557 and an issue with Propers for complement	msozeau	2011-10-07
*	- Make typeclass transparency information directly available	msozeau	2011-04-13
*	- Do not make constants with an assigned type polymorphic (wrong unfoldings).	msozeau	2011-04-13
*	- 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
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Fix bug #2321, allowing "_" named projections in classes. Not realizing	msozeau	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove compile-command pragmas for emacs	letouzey	2010-05-19