coq - The formal proof system

Age	Commit message (Expand)	Author
2006-08-29	Ajout (pour complétude) du cas d'inversion d'un pattern de Miller vis	herbelin
2006-08-29	Prise en compte de l'instance des evars dans la détection des 'motifs'	herbelin
2006-08-29	Il faut (au moins) normaliser les evars avant de tenter	herbelin
2006-08-28	Diverses modifications autour de l'unification modulo conversion:	herbelin
2006-08-28	Ajout whd_eta + export append_stack_list + petit nettoyage (dont maj de	herbelin
2006-08-24	Morceau de code mort	herbelin
2006-07-22	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir
2006-07-07	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin
2006-06-27	Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...	herbelin
2006-06-22	Added {measure x f} as a valid recursion order.	msozeau
2006-06-19	bug serieux efficacite de ltac	barras
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-05-28	- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-05-19	Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort	herbelin
2006-05-17	Correcting a bug in matching context on if.	jforest
2006-05-13	Code mort	herbelin
2006-05-10	correction bugs dans Cbv (beta n-aire)	barras
2006-05-09	subst. explicites avec vecteurs	barras
2006-05-05	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras
2006-04-28	Standardisation du nom des méthodes de Evd	herbelin
2006-04-28	Typo dans précédent commit (8755); protection renforcée dans analyse claus...	herbelin
2006-04-27	- Distinction explicite des parties paramètres et arguments dans le type	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
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