coq - The formal proof system

Age	Commit message (Expand)	Author
2017-03-07	Farewell decl_mode	Enrico Tassi
2016-05-04	Moving the Val module to Geninterp.	Pierre-Marie Pédrot
2016-02-22	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-03-13	rewiring Czar printers that were disabled	Pierre Corbineau
2015-01-12	Update headers.	Maxime Dénès
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey
2012-03-02	Noise for nothing	pboutill
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