coq - The formal proof system

Age	Commit message (Expand)	Author
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
1999-10-19	les variables existentielles contiennent maintenant un environnement (type	filliatr
1999-10-18	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr
1999-10-14	module Logic	filliatr
1999-10-14	module Proof_trees	filliatr
1999-10-13	redeplacement des var. ex. dans kernel :-)	filliatr
1999-10-08	module Logic (ne compile pas encore)	filliatr