coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Notations:	herbelin	2006-10-09
*	Remplacement des nf_evar (source de complexité polynomiale) par de la	herbelin	2006-10-06
*	Déplacement de on_judgment_type de Typeops vers Termops	herbelin	2006-10-06
*	Suppression d'une source de complexité polynomiale dans le pretypage	herbelin	2006-10-06
*	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin	2006-10-05
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
*	Ajout allowed_sorts	herbelin	2006-10-01
*	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin	2006-09-23
*	Correction bug #1168 (dans les coercions de pattern, c'est le nombre	herbelin	2006-09-23
*	Wish #1187 granted (support for canonical structures that are records	herbelin	2006-09-23
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin	2006-09-15
*	Débogage: ajout affichage contraintes d'unification	herbelin	2006-09-15
*	Abandon unification pattern des evars dans apply: combiné avec le	herbelin	2006-09-13
*	Correction conflit Meta/Evar dans commit précédent et extension au	herbelin	2006-09-12
*	Ajout unification pattern dans l'algorithme d'unification des	herbelin	2006-09-12
*	Workaround Map.fold semantic change in ocaml-3.08.4 and higher.	msozeau	2006-09-05
*	Ajout is_sort: test si se réduit en une sorte	herbelin	2006-09-01
*	Export de check_evars vers command.ml	herbelin	2006-09-01
*	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-29
*	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-28
*	Morceau de code mort	herbelin	2006-08-24
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22
*	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin	2006-07-07
*	Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...	herbelin	2006-06-27
*	Added {measure x f} as a valid recursion order.	msozeau	2006-06-22
*	bug serieux efficacite de ltac	barras	2006-06-19
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin	2006-05-30
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
*	- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites	herbelin	2006-05-28
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort	herbelin	2006-05-19
*	Correcting a bug in matching context on if.	jforest	2006-05-17
*	Code mort	herbelin	2006-05-13
*	correction bugs dans Cbv (beta n-aire)	barras	2006-05-10
*	subst. explicites avec vecteurs	barras	2006-05-09
*	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras	2006-05-05
*	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-28
*	- 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-27
*	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin	2006-04-26
*	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
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14