coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix exponential behaviour of the typeclasses persistent objects. Drop	puech	2008-12-06
*	Fixes for unification and substitution of metas under binders.	msozeau	2008-12-04
*	improved simpl	barras	2008-12-03
*	Miscellaneous fixes and improvements:	herbelin	2008-12-02
*	another bug with simpl	barras	2008-11-28
*	Fix (?) a pattern matching compilation problem:	msozeau	2008-11-27
*	fixed bug 1791: simpl was performing eta expansion	barras	2008-11-27
*	fixing problem with CompCert: reordering resulting from tac change was not cl...	barras	2008-11-27
*	fixed problem with r11612	barras	2008-11-21
*	fixed exponential behavior of evar unif (ground case)	barras	2008-11-21
*	Restores behaviour of v8.1 for unification problems which fail (backport of 1...	letouzey	2008-11-14
*	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin	2008-11-09
*	Apply vmconv if there are no _undefined_ evars around.	msozeau	2008-11-08
*	Slight change of the semantics of user-given casts: they don't really	msozeau	2008-11-07
*	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau	2008-11-07
*	Fix in the unification algorithm using evars: unify types of evar	msozeau	2008-11-05
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05
*	Fixes and refinements regarding occurrence selection:	herbelin	2008-10-26
*	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin	2008-10-26
*	More debugging of handling of open constrs with typeclasses:	msozeau	2008-10-25
*	Open notation for declaring record instances.	msozeau	2008-10-23
*	Retour en arrière pour raison de compatibilité sur la suppression du nf_evar	herbelin	2008-10-19
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	* Fixed constr_cmp again to handle universes subtyping correctly	puech	2008-10-09
*	fixing r11433 again:	barras	2008-10-07
*	(Try to) use the conversion oracle also in w_unify to choose which constant to	msozeau	2008-10-03
*	Fixing constr_cmp, propagating subtyping only right of a product	puech	2008-10-02
*	Correcting a delta normalization bug in VM (checked by benjamin)	jforest	2008-09-30
*	Partial fix for bug #1948: recompute order of dependencies between	msozeau	2008-09-25
*	Fix bug #1943 and restrict the inference optimisation of Program to	msozeau	2008-09-15
*	Fix bug #1936: uncaught exception due to undefinable exceptions.	msozeau	2008-09-14
*	Fix bug #1940: uncaught exception when searching for a type class.	msozeau	2008-09-14
*	Fix a bug, in fold_constr_with_binders, the types of fixpoints were	msozeau	2008-09-13
*	Better handling of the opacity of proof obligations, add the possibility of	msozeau	2008-09-07
*	Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving an	msozeau	2008-09-04
*	Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about	herbelin	2008-09-02
*	Fix implementation of "Global Instance" which redeclared the same	msozeau	2008-08-27
*	Correction de bugs:	herbelin	2008-08-05
*	Correction bug de filtrage sous-terme #1920 introduit dans commit	herbelin	2008-08-05
*	Suite 11187 et 11298 : ne retarder le dépliage d'une projection	herbelin	2008-08-05
*	Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par	herbelin	2008-08-04
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Corrige un bug du commit 11187 (le comportement à respecter était	herbelin	2008-07-31
*	Backport r11289.	msozeau	2008-07-29
*	Fix bug in term dnet preventing some unifications. Allow "higher-order"	msozeau	2008-07-28
*	Even better test for choosing rewrite or setoid_rewrite.	msozeau	2008-07-26
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	broke cyclic dependencies	barras	2008-07-24
*	A try at allowing matching on applications as a binary syntax node by default.	msozeau	2008-07-22
*	Correct implementation of discharging of implicit arguments and add new	msozeau	2008-07-22