coq - The formal proof system

Age	Commit message (Expand)	Author
2004-09-15	hiding the meta_map in evar_defs	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-09-19	Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...	herbelin
2001-03-15	entetes	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-06-29	Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_of	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-01-28	documentation	filliatr
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-09	Ajout des messages d'erreurs de Cases	herbelin
1999-12-03	- global_reference traite des variables	filliatr
1999-12-01	Retour dans pretyping	herbelin
1999-12-01	déplacé dans kernel	herbelin
1999-12-01	- environment -> safe_environment	filliatr
1999-11-26	Version initiale	herbelin