coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2009-02-06	pushed evar reduction in kernel	barras
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2004-11-12	Changement dans les boxed values .	gregoire
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-08	unification encore...	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-10-10	Unification lemInv et lemInv_in	herbelin
2002-12-24	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin
2002-12-19	suite du commit precedent	barras
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2002-02-07	petit nettoyage de kernel/inductive	barras
2002-02-01	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-08-05	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin
2001-07-10	Branchement sur bad_tactic_args	herbelin
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin
2000-12-13	conflit useInversionLemma	mohring
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-04	caractere opaque des constantes repris en compte	filliatr
2000-11-06	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr
2000-11-02	correction Abstract (et make world passe!)	filliatr
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-10-18	Renommage canonique :	herbelin
2000-09-14	Abstraction de constr	herbelin