coq - The formal proof system

Age	Commit message (Expand)	Author
2016-06-09	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-11-20	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-11-18	Inlining the only use of Clenv.connect_clenv.	Pierre-Marie Pédrot
2015-11-17	Performance fix for destruct.	Pierre-Marie Pédrot
2015-02-02	Removing dead code.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-10-27	Cleaning and documenting Clenv.make_evar_clause	Pierre-Marie Pédrot
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-10-21	Lazily check that an argument is dependent when constructing evar clauses.	Pierre-Marie Pédrot
2014-10-21	Adding an evar version of the make_clenv function.	Pierre-Marie Pédrot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2014-04-22	Simplifying interface of elimination tactics. They used dummy clausenvs, and	Pierre-Marie Pédrot
2014-03-26	Moving some tactic code to the new engine.	Pierre-Marie Pédrot
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-09-25	Removing useless evar-related stuff.	ppedrot
2013-06-04	Backtrack on unneeded change of interface for pose_metas_as_evars.	msozeau
2013-06-04	Start documenting new [rewrite_strat] tactic that applies rewriting	msozeau
2013-04-29	Merging Context and Sign.	ppedrot
2012-08-08	Updating headers.	herbelin
2012-05-29	remove many excessive open Util & Errors in mli's	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-03-02	Noise for nothing	pboutill
2011-06-21	Cleaning debugging printer relative to new proof engine. In	herbelin
2011-06-10	Moved allow_K to a unification flag	herbelin
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-09-17	In the computation of missing arguments for apply, accept that the	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-13	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin
2010-06-09	Fix bug #2317: setoid_rewrite ignored binding lists. Slightly	msozeau
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2004-09-03	deplacement de clenv vers pretyping	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-10-10	Suppression clenv_change_head que seul Wcclausenv utisait	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-19	suite du commit precedent	barras
2002-10-01	Vraie substitutivite de autohints	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-04-12	Re-introduction de clenv_constrain_missing_arg utilisé par la contrib Lannion	herbelin
2002-04-11	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin
2002-04-10	backtrack dans l'algo d'unification	barras
2002-04-03	transformation des evar en meta preserve la linearite des metas	barras
2002-04-02	- modifs de la condition de garde pour mieux tenir compte des raisonnements	barras