coq - The formal proof system

Age	Commit message (Expand)	Author
2016-11-07	More explicit name for status of unification constraints.	Maxime Dénès
2016-07-13	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot
2016-07-13	Fixing printing of evar name in an error message of instantiate.	Hugo Herbelin
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-03-20	Extruding the code for the Existential command from Proofview.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-04-23	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-08-07	Better structure for Ltac pretyping environments.	Pierre-Marie Pédrot
2014-08-06	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack
2013-12-17	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-06-22	Generalizing the use of maps instead of lists in the interpretation	ppedrot
2013-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey
2013-02-17	Added propagation of evars unification failure reasons for better	herbelin
2013-01-29	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin
2012-11-25	Monomorphization (proof)	ppedrot
2012-09-14	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-08-08	Updating headers.	herbelin
2012-05-29	Glob_term now mli-only, operations now in Glob_ops	letouzey
2012-03-14	Revise API of understand_ltac to be parameterized by a flag for resolution of...	msozeau
2012-03-14	Second step of integration of Program:	msozeau
2012-03-02	Noise for nothing	pboutill
2011-03-07	Reverted commit r13893 about propagation of more informative	herbelin
2011-03-07	Added propagation of evars unification failure reasons for better	herbelin
2011-02-17	- Use transparency information all the way through unification and	msozeau
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-10-30	Take constraints into account in the "instantiate" tactic	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
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-08-04	Évolutions diverses et variées.	herbelin
2008-06-03	Fixes incorrect handling of existing existentials variables in	msozeau
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-04-26	Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et unifo...	notin
2007-02-01	Report de révision 9583 de la v8.1 dans le trunk	notin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-04-28	Standardisation du nom des méthodes de Evd	herbelin
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2005-12-21	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin