coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction pbs liés aux evar	herbelin	2000-01-07
*	Déplacement non-affichage des coercions dans termast	herbelin	2000-01-07
*	Bug lift	herbelin	1999-12-15
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
*	- états fabriqués avec -silent	filliatr	1999-12-13
*	- méthode load sur les Hints	filliatr	1999-12-13
*	Poursuite intégration du Cases	herbelin	1999-12-13
*	Intégration initiale du Cases	herbelin	1999-12-11
*	Quelques fonctions sur les locations des rawconstr	herbelin	1999-12-11
*	- erreurs Pretype	filliatr	1999-12-10
*	Suppression Rel de rawconstr et correction de bugs d'affichage	herbelin	1999-12-10
*	Ajout des messages d'erreurs de Cases	herbelin	1999-12-09
*	changement type add_anonymous_leaf	filliatr	1999-12-05
*	- global_reference traite des variables	filliatr	1999-12-03
*	Modifs suite à intégration de class.ml	herbelin	1999-12-02
*	... dans toplevel	herbelin	1999-12-02
*	modifs pour premiere edition de liens	filliatr	1999-12-02
*	affichage classes et coercions	filliatr	1999-12-02
*	Intégration du Termast et du Retyping de HH, et modifications connexes	herbelin	1999-12-01
*	Renommage de multcase en cases	herbelin	1999-12-01
*	Retour dans pretyping	herbelin	1999-12-01
*	déplacé dans kernel	herbelin	1999-12-01
*	mise au point Declare et avancee dans Astterm	filliatr	1999-12-01
*	mise a jour Coercion	filliatr	1999-12-01
*	- environment -> safe_environment	filliatr	1999-12-01
*	- Typing -> Safe_typing	filliatr	1999-12-01
*	inductive_key et constructor_key	herbelin	1999-11-30
*	ocamlweb	filliatr	1999-11-30
*	ocamlweb	filliatr	1999-11-30
*	portage modules Evarconv et Evarutil	filliatr	1999-11-29
*	portage Astterm (partiellement)	filliatr	1999-11-29
*	fin Recordops, et debut Evarutil	filliatr	1999-11-27
*	Pas encore pret	herbelin	1999-11-26
*	Modification pour faire compiler pretyping.ml qui maintenant compile	herbelin	1999-11-26
*	Maintenant compilable	herbelin	1999-11-26
*	Version initiale	herbelin	1999-11-26
*	module Classops; ajout de fonctions dans Declare en consequence	filliatr	1999-11-26
*	Des progres dans l'integration	herbelin	1999-11-25
*	MAJ pour fusion avec pretyping	herbelin	1999-11-24
*	Versions initiales	herbelin	1999-11-24
*	Deplace dans parsing	herbelin	1999-11-24
*	Version initiale	herbelin	1999-11-24
*	Version préliminaire	herbelin	1999-11-19
*	pas de grosse banniere; pas de double point-virguke	filliatr	1999-11-18
*	Traducteur ast -> rawterm	herbelin	1999-10-24
*	Type ML des termes non prétypés	herbelin	1999-10-24
*	organisation de trad (entre parsing/ et pretyping/)	filliatr	1999-10-13