coq - The formal proof system

Age	Commit message (Expand)	Author
2014-03-26	Adding an interface to Eqdecide and putting the grammar rules in a dedicated	Pierre-Marie Pédrot
2014-03-02	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey
2014-02-27	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack
2013-12-02	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot
2013-11-25	Remove the Hiddentac module.	Arnaud Spiwack
2013-11-02	Fixing CAMLP4 compilation.	ppedrot
2013-11-02	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack
2013-11-02	More Proofview.Goal.enter.	aspiwack
2013-11-02	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack
2013-11-02	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2012-12-14	Modulification of identifier	ppedrot
2012-10-15	Continue killing hidden tactics : no more generated h_xxx	letouzey
2012-10-06	remove Refiner.abstract_tactic and similar	letouzey
2012-10-06	Clean-up : removal of Proof_type.tactic_expr	letouzey
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-08-08	Updating headers.	herbelin
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey
2012-03-02	Noise for nothing	pboutill
2010-12-24	tactics/eqdecide.ml4: avoid a useless argument in decideEquality	glondu
2010-12-23	Remove the two-argument variant of "decide equality"	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-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-06-07	- Added two new introduction patterns with the following temptative syntaxes:	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-03-22	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin
2006-01-28	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-11-02	Types inductifs parametriques	mohring
2004-07-16	Nouvelle en-tête	herbelin
2003-05-19	Restructuration des procédures de filtrage	herbelin
2003-04-16	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2002-06-05	Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...	herbelin
2002-06-05	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...	herbelin
2002-05-29	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin