coq - The formal proof system

Age	Commit message (Expand)	Author
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-05-23	A try at using sort variables during unification. Instead of refreshing	msozeau
2009-04-08	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin
2008-10-18	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin
2008-10-07	fixing r11433 again:	barras
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-05-28	- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites	herbelin
2006-03-29	Inductifs avec polymorphisme de sorte (version initiale)	herbelin
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