coq - The formal proof system

Age	Commit message (Expand)	Author
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
2002-03-21	backtrack de l'unification	barras
2002-03-20	encore quelques petites modif de l'unification	barras
2002-03-08	renommage de fonctions	barras
2002-03-04	Nouveau Rewrite-in plus economique	barras
2001-11-12	Suppression des stamps et donc des *_constraints	clrenard
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-10	Incompatibilité entre la prise en compte des univers au niveau des tactiques...	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-06-29	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-03-01	backtrack unification types et deplacement make_clenv_binding	filliatr
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	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-03	- coqmktop	filliatr
1999-11-24	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr
1999-11-22	module Wcclausenv	filliatr
1999-10-20	module Clenv (debut)	filliatr