coq - The formal proof system

Age	Commit message (Expand)	Author
2006-04-26	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin
2006-04-25	Reverting nf_betaiotaevar_preserving_vm_cast	jforest
2006-04-25	Code mort (suite)	herbelin
2006-04-25	Suppression code mort	herbelin
2006-04-24	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-04-14	Pas fier	herbelin
2006-04-14	replacing whd_betaiotaevar_preserving_vm_cast	jforest
2006-04-10	Fixes for new unification, not used in default version as it really changes u...	msozeau
2006-04-10	Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...	msozeau
2006-04-07	- Documentation of the Program tactics.	msozeau
2006-03-29	Inductifs avec polymorphisme de sorte (version initiale)	herbelin
2006-03-28	Correction bug/typo dans splay_prod_assum et ajout decomp_sort	herbelin
2006-03-22	Subtac fixes, single fixpoint definitions are working again. Added a toggle o...	msozeau
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2006-03-22	- Correction bug calcul mind_consnrealargs, introduit à la révision	herbelin
2006-03-17	Modification des propriétés (svn:executable)	notin
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-03-04	Correction message d'erreur ltac et adoption du modèle de message de Tacinterp	herbelin
2006-03-02	Correctif pour bug #1089 (cannot define an isevar twice)	herbelin
2006-02-08	Localisation des erreurs de sorte du prétypage	herbelin
2006-02-07	oubli de code de debugging	herbelin
2006-02-07	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin
2006-02-07	Mise en conformité de l'ordre des occurrences de pattern avec l'affichage	herbelin
2006-02-01	Optimisation filtrage sans lieurs (utile pour Ltac)	herbelin
2006-01-30	Suppression fonctions d'interprétation du vieux Case	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	Fonctions retournant les arits des constructeurs et inductifs	herbelin
2006-01-30	- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;	herbelin
2006-01-29	Documentation	herbelin
2006-01-16	Version préliminaire d'inversion de la compilation du filtrage	herbelin
2006-01-11	Standardisation du nom de subst_raw en subst_rawconstr	herbelin
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2006-01-11	Suppression résidus code v7 et traducteur	herbelin
2006-01-10	Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...	herbelin
2006-01-08	Fonctions de conversion rawconstr <-> cases_pattern	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-21	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2005-12-17	Orthographe de 'instantiate'	herbelin
2005-12-05	changement d'egalite pour le named_context_val	gregoire
2005-12-02	Changement des named_context	gregoire
2005-11-28	parametres inductifs	mohring
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-02	Types inductifs parametriques	mohring
2005-11-02	Correction bug invert_names (cf bug #1031)	herbelin
2005-09-09	Léger nettoyage et uniformisation + généralisation du point d'entrée ltac...	herbelin