coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_...	herbelin	2004-07-11
*	Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ...	herbelin	2004-07-11
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30
*	Essai de suppression de eta dans simpl (cf bug #779)	herbelin	2004-06-29
*	Double bug d'affichage des cases dépendants (bug #784)	herbelin	2004-06-28
*	Correction affichage v8 des records avec let (bug #798)	herbelin	2004-06-27
*	correspondance des records et noms de champs de records entre un module et sa...	letouzey	2004-06-25
*	test de conversion laissait echapper exception NotConvertible	barras	2004-05-14
*	Terminologie plus intuitive: evaluable -> unfoldable	herbelin	2004-04-30
*	Prise en compte d'un type dont la sorte est une evar	herbelin	2004-04-29
*	Correction incapacité à gérer les annotations de type dépendantes pour le...	herbelin	2004-04-27
*	Correction confusion entre la dependance en les termes filtrees dans l'annota...	herbelin	2004-04-13
*	bug #606: mis un message d'erreur plus clair	barras	2004-04-07
*	Déclaration des record au chargement (ce n'est pas une question de visibilit...	herbelin	2004-04-05
*	Typo	herbelin	2004-03-29
*	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...	herbelin	2004-03-28
*	bug de PP des fix (coqbugs #574)	barras	2004-03-24
*	preparation pour release (suite)	barras	2004-03-15
*	bug affichage des cofix	barras	2004-03-09
*	correction de bugs des points fixes	barras	2004-03-08
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Erreur de Bruijn et oubli substitution alias dans annotation du 'match'	herbelin	2004-02-27
*	Inclusion des annotations de type des filtrages dans 'Set Printing All'	herbelin	2004-02-26
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	Deplacement array_map_left and co dans Util	herbelin	2004-02-13
*	Bug numerotation des occurrences pour 'simpl id at n' (suite)	herbelin	2004-02-13
*	Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...	herbelin	2004-02-13
*	On s'affranchit de l'information inductif ou pas dans le prédicat (càd	herbelin	2004-02-05
*	Suppression des types dans la signature du predicat (ils sont	herbelin	2004-02-05
*	Reconnaissance précoce de la dépendance du prédicat en un terme filtré	herbelin	2004-02-04
*	Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...	herbelin	2004-02-04
*	Relachement condition pour declarer un inductif dans la table des 'If'; contr...	herbelin	2004-02-03
*	Backtrack sur recuperation de noms a partir du type, car casse la correction ...	herbelin	2004-02-03
*	Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...	herbelin	2004-01-29
*	Reparation d'une rupture (en presence de types implicites) de l'invariant que...	herbelin	2004-01-29
*	Bug (destruct/induction ne savent pas traiter le cas non atomique avec param�...	herbelin	2004-01-27
*	Set is not always impredicative	barras	2004-01-12
*	Type le 'return' comme un type	herbelin	2003-12-27
*	Affichage opaque	herbelin	2003-12-23
*	Substitution dans REvar; reparation bug 277	herbelin	2003-12-19
*	Substitution dans REvar et PEvar plutot que encodage via noeud application po...	herbelin	2003-12-19
*	Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'	herbelin	2003-12-17
*	Correction bug 371 (sub_match retournait des instances non closes)	herbelin	2003-12-16
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Bug introduit avec le 'Simpl f'	herbelin	2003-11-22
*	Ajout 'Simpl f'	herbelin	2003-11-21
*	Deplacement subst_rawconstr dans Rawterm	herbelin	2003-11-19
*	Ajout mis_constructor_nargs_env	herbelin	2003-11-18
*	Ajout reduce_to_quantified_ref	herbelin	2003-11-09
*	Amelioration message d'erreur pour ltac	herbelin	2003-11-04