coq - The formal proof system

Age	Commit message (Expand)	Author
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