coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-24	Add a new evar source to refer to evars which are types of evars.	Hugo Herbelin
2018-04-26	Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.	Hugo Herbelin
2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin
2017-10-19	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann
2017-06-08	Merge branch 'v8.6'	Pierre-Marie Pédrot
2017-06-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-05-28	Fixing a subtle bug in tclWITHHOLES.	Hugo Herbelin
2015-01-01	An optimization in the use of unification candidates so as to get the	Hugo Herbelin
2014-12-10	Fixing orientation of postponed subtyping problems.	Hugo Herbelin
2014-12-07	Improving evar restriction (this is a risky change, as I remember a	Hugo Herbelin
2013-03-21	Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.	herbelin
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-11-28	Evarconv: Fix #2936 + comments	pboutill
2012-06-12	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot
2012-03-26	Unification: Added a heuristic to solve problems of the form	herbelin
2012-01-04	Type inference unification: fixed a 8.4 bug in the presence of unification	herbelin
2011-12-04	Discarding let-ins from the instances of the evars in the	herbelin
2011-10-24	Fixing another bug revealing ill-typed use of evar restriction.	herbelin
2011-03-05	Improved define_evar_as_lambda which was creating an unrelated new evar	herbelin
2010-09-30	Improve handling of metas as evars in unification (patch by Hugo)	letouzey
2009-10-30	Attempt to capture on time unification errors for "with" bindings.	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-04-25	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin
2009-02-06	From v8.2 to trunk:	herbelin
2008-08-05	Correction de bugs:	herbelin
2008-06-29	Préférence donnée aux constantes qui ne sont pas des projections	herbelin
2008-06-18	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin
2007-09-26	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin
2007-09-18	Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-16	Réponse à une incompatibilité introduite dans 10114 (calcul du nombre	herbelin
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-05-28	Adaptation au passage de option dans Type	herbelin
2006-03-05	Ajout test relatif au bug #984	herbelin
2006-03-02	Ajout test bug 1089	herbelin
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
2004-12-08	Ajout bug do_restrict_hyp	herbelin
2004-04-29	Test bug 705	herbelin
2003-01-19	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin
2001-11-21	La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...	herbelin
2001-11-16	* empty log message *	herbelin
2001-03-15	entetes	filliatr
2001-03-14	* empty log message *	herbelin