coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	préparation de add_glob en vue d'isolement de la partie module pour	herbelin	2006-04-27
*	Ajout chop_dirpath	herbelin	2006-04-27
*	2-3 lemmes en plus pour que les Bvectors soient effectivement utilisables	letouzey	2006-04-27
*	Added a short doc for "Function". To be finished.	courtieu	2006-04-27
*	MAJ	herbelin	2006-04-26
*	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin	2006-04-26
*	Outil de test de la réversibilité du réafficheur v8->v8	herbelin	2006-04-26
*	Diverses corrections de l'afficheur et du traducteur pour s'assurer de	herbelin	2006-04-26
*	Régénération après mise à jour coqdep pour traiter Require multiple	herbelin	2006-04-26
*	Prise en compte du Require multiple	herbelin	2006-04-26
*	suite du pont entre Bvector et N	letouzey	2006-04-26
*	Replacing "GenFixpoint" with "Function" and "mes" with "measure"	jforest	2006-04-26
*	Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la créat...	notin	2006-04-26
*	Un gros coup de lifting pour IntMap:	letouzey	2006-04-25
*	un lemme de double inclusion	letouzey	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-25
*	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin	2006-04-24
*	Changement anomaly en failwith dans out_name pour utilisation par map_succeed	herbelin	2006-04-24
*	Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;	herbelin	2006-04-24
*	+ Handling "if" and cast in GenFixpoint	jforest	2006-04-24
*	decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)	letouzey	2006-04-20
*	Nouveau mécanisme pour les modules interactifs : les arguments de	herbelin	2006-04-16
*	Added code to support "Program Lemma/Example... etc"	msozeau	2006-04-16
*	Inversion de l'ordre de chargement des objets logiques et non logiques	herbelin	2006-04-15
*	Tests notations	herbelin	2006-04-15
*	Test synchronisation chargement objets non logiques	herbelin	2006-04-15
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14
*	Pas fier	herbelin	2006-04-14
*	mise a jour credits	cpaulin	2006-04-14
*	Enleve les commentaires	cpaulin	2006-04-14
*	Test files for subtac.	msozeau	2006-04-14
*	Maj configure, README, etc...	notin	2006-04-14
*	Premier jet annonce 8.1	herbelin	2006-04-14
*	MAJ 8.1	herbelin	2006-04-14
*	replacing whd_betaiotaevar_preserving_vm_cast	jforest	2006-04-14
*	MAJ 8.1-APP	herbelin	2006-04-13
*	MAJ 8.1-APP	herbelin	2006-04-13
*	Changement de licence pour le Tutoriel de Coq	notin	2006-04-12
*	Simplifying the proof of principles	jforest	2006-04-12
*	induction on multiple arguments made better:	courtieu	2006-04-12
*	Modification of "Show Intros": it now shows letins too.	courtieu	2006-04-11
*	adding a new tactic [intro_avoiding idl] which acts as intro but prevents the	jforest	2006-04-11
*	ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release)	courtieu	2006-04-11
*	patch pour contourner l'échec de type_of_applied_inductive sur un inductif a...	herbelin	2006-04-11
*	Fixes for new unification, not used in default version as it really changes u...	msozeau	2006-04-10
*	+ Changing a little functional schemes types	jforest	2006-04-10
*	Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...	msozeau	2006-04-10
*	New unification can solve the problem without eta-expansion,	msozeau	2006-04-10