coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-21	Generic support for open terms in tactics	herbelin
2009-09-18	- Fixed a bug in checking that implicit arguments are all correctly	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-07-07	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack
2009-06-02	Backtrack on experimental unification with sort variables: it requires	msozeau
2009-05-23	A try at using sort variables during unification. Instead of refreshing	msozeau
2009-05-18	Minor unification changes:	msozeau
2009-04-24	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin
2009-02-19	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack
2008-12-14	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-25	More debugging of handling of open constrs with typeclasses:	msozeau
2008-10-24	Raise informative errors instead of Failures or anomalies in case a meta	msozeau
2008-10-18	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2008-04-27	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin
2008-04-26	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2008-04-17	Bug squashing day !	msozeau
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2008-03-16	Using the "relation" constant made some unifications fail in the new	msozeau
2008-02-13	Essai de prise en compte de delta dans unify_0 (même sur termes non clos).	herbelin
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2006-02-10	induction now admits multiple induction arguments. The principle must	coq
2005-12-02	Changement des named_context	gregoire
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-10	simplification de clenv	barras
2004-09-08	unification encore...	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	premiere reorganisation de l\'unification	barras