coq - The formal proof system

Age	Commit message (Expand)	Author
2016-09-24	Moving "move" in the new proof engine.	Hugo Herbelin
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
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-01-12	Update headers.	Maxime Dénès
2014-10-09	A version of convert_concl and convert_hyp in new proof engine.	Hugo Herbelin
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2014-01-06	Algebraized "No such hypothesis" errors	Pierre-Marie Pédrot
2013-04-29	Merging Context and Sign.	ppedrot
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-08-08	Updating headers.	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-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
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2008-10-24	Raise informative errors instead of Failures or anomalies in case a meta	msozeau
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2007-01-22	Correction du bug #1315:	notin
2006-03-01	Correction bug #842 (rename d'une hyp du contexte)	herbelin
2005-03-19	Correction erreur grossière de non restauration d'état en cas de retour exc...	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
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
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-09	Option pour rendre les vérifications du refiner optionnelle	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-06	Ajout erreur DoesNotOccurIn	herbelin
2000-09-14	Abstraction de constr	herbelin
2000-07-25	retablissement make doc et make minicoq	filliatr
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclaration...	herbelin
2000-05-18	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
1999-12-14	rattrapage exceptions autres que UserError	filliatr
1999-12-01	module Pfedit	filliatr
1999-12-01	- Typing -> Safe_typing	filliatr
1999-11-23	modules Indrec, Tacentries, Hiddentac	filliatr
1999-11-22	module Wcclausenv	filliatr
1999-11-22	module Tactics (debut)	filliatr
1999-10-20	module Clenv (debut)	filliatr