coq - The formal proof system

Age	Commit message (Expand)	Author
2006-02-06	coq_makefile	herbelin
2006-02-06	Ajout de l'essai d'effacement des noms des cibles custom par la cible clean	herbelin
2006-02-05	maj	coq
2006-02-05	Debugging en syntaxe v8	herbelin
2006-02-04	maj	coq
2006-02-04	Branchement sur nouvelle interface de declare_numeral_interpreter	herbelin
2006-02-04	Recherche des global_reference paresseusement pour pouvoir interpréter	herbelin
2006-02-04	parsing/g_ascii_syntax.ml	herbelin
2006-02-04	Ajout nat_path et find_reference	herbelin
2006-02-04	Utilisation du section_path pour le parsing des notations primitives,	herbelin
2006-02-04	code mort	herbelin
2006-02-03	maj	coq
2006-02-03	added mli 's for the nex functional induction (forgotten last time).	coq
2006-02-03	+ Adding an error message when the function cannot be defined	bertot
2006-02-02	maj	coq
2006-02-01	maj	coq
2006-02-01	protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)	barras
2006-02-01	protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)	barras
2006-02-01	New version of functional induction / inversion. By Julien Forest,	coq
2006-02-01	Optimisation filtrage sans lieurs (utile pour Ltac)	herbelin
2006-01-31	maj	coq
2006-01-31	Adaptation message d'erreur au cas des string	herbelin
2006-01-31	Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char	herbelin
2006-01-31	Ajout décidabilité	herbelin
2006-01-30	maj	coq
2006-01-30	Suppression fonctions d'interprétation du vieux Case	herbelin
2006-01-30	Prise en compte coercions autour des sous-termes filtrés (si non dépendants)	herbelin
2006-01-30	Gestion des erreurs pour nombre incorrect d'argument des constructeurs (et de	herbelin
2006-01-30	- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer	herbelin
2006-01-30	Fonctions retournant les arits des constructeurs et inductifs (suite)	herbelin
2006-01-30	Déplacement du test du bon nombre d'argument des constructeurs (et de	herbelin
2006-01-30	Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas la	herbelin
2006-01-30	Fonctions retournant les arits des constructeurs et inductifs	herbelin
2006-01-30	Nettoyage warning (dont flush et affichage seulement si mode verbose)	herbelin
2006-01-30	- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;	herbelin
2006-01-30	Ajout ppenv	herbelin
2006-01-30	Plutôt pas de contraction des match dans le déboggueur	herbelin
2006-01-29	maj	coq
2006-01-29	Documentation	herbelin
2006-01-29	Ajout printer Idset.t	herbelin
2006-01-29	Bug 'match x in I' (potentiellement utilisable comme cast)	herbelin
2006-01-29	MAJ (synonymes de Lemma; auto using)	herbelin
2006-01-29	Ajout syntaxe concrète Proposition, synonyme de Lemma	herbelin
2006-01-28	maj	coq
2006-01-28	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin
2006-01-28	- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma	herbelin
2006-01-28	- Ajout syntaxe concrète Property/Corollary, synonymes de Lemma	herbelin
2006-01-28	Correction bug Inspect introduit par le passage du discharge à une méthode ...	herbelin
2006-01-28	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin
2006-01-28	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin