coq - The formal proof system

Age	Commit message (Expand)	Author
2006-11-29	correction du bug : VM value extraction error (PR#1290)	bgregoir
2006-11-22	Code mort découvert par Matthieu	herbelin
2006-11-19	Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après	herbelin
2006-11-19	Raffinement de l'unification de "apply": mémorisation de certains	herbelin
2006-11-18	Code mort (duplication de code dans reductionops.ml)	herbelin
2006-11-03	Suppression source de complexité polynomiale introduite par le polymorphisme	herbelin
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-25	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin
2006-10-25	Suite commit 9277	herbelin
2006-10-25	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin
2006-10-24	Ajout de la tactique "apply in".	herbelin
2006-10-21	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin
2006-10-21	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin
2006-10-09	Notations:	herbelin
2006-10-06	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-05	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-01	Ajout allowed_sorts	herbelin
2006-09-23	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-20	Declarative Proof Language: main commit	corbinea
2006-09-15	Report de l'heuristique d'unification premier ordre flexible/rigide	herbelin
2006-09-15	Débogage: ajout affichage contraintes d'unification	herbelin
2006-09-13	Abandon unification pattern des evars dans apply: combiné avec le	herbelin
2006-09-12	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-05	Workaround Map.fold semantic change in ocaml-3.08.4 and higher.	msozeau
2006-09-01	Ajout is_sort: test si se réduit en une sorte	herbelin
2006-09-01	Export de check_evars vers command.ml	herbelin
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