coq - The formal proof system

Age	Commit message (Expand)	Author
2006-09-14	Correction du bug #1181	jforest
2006-09-14	Compilation de Coq sous Windows	notin
2006-09-14	mise en conformite des messages d'erreur de Function avec la doc.	jforest
2006-09-14	Modification de l'appel aux exécutables Caml	notin
2006-09-13	Abandon unification pattern des evars dans apply: combiné avec le	herbelin
2006-09-12	Indentation + svnprop	notin
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-12	Ajout array_distinct	herbelin
2006-09-11	Ajout eassumption index	herbelin
2006-09-09	Retour à un warning en cas de (co-)fixpoint pas totalement mutuel	herbelin
2006-09-07	Updating the doc about Function and co	courtieu
2006-09-06	Finalement, interdiction des points fixes non totalement mutuellement	herbelin
2006-09-05	Code mort	herbelin
2006-09-05	Workaround Map.fold semantic change in ocaml-3.08.4 and higher.	msozeau
2006-09-04	Fix wrong order for building library, add informative messages.	msozeau
2006-09-01	New handling of obligations.	msozeau
2006-09-01	Correction bug d'ordonnancement des hyps d'induction dans induction/destruct	herbelin
2006-09-01	Forgot to add this one.	msozeau
2006-09-01	Subtac fixes, new way of handling obligations in progress.	msozeau
2006-09-01	Coq ne compile plus avec OCaml 3.06 (mais avec 3.07 c'est ok)	notin
2006-09-01	Suite ajout option -ocamlib à configure	notin
2006-09-01	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin
2006-09-01	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin
2006-09-01	Force évaluation 'naturelle' de list_map2_i et list_map3 de gauche à droite	herbelin
2006-09-01	MAJ	herbelin
2006-09-01	Ajout possibilité clause "where" dans co-points fixes	herbelin
2006-09-01	Affichage de l'aide dans configure	notin
2006-09-01	Extension et réorganisation de l'interprétation des (co-)points fixes	herbelin
2006-09-01	Export de fonctions d'interprétation acceptant des evars non résolues	herbelin
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-09-01	Indentation + typo	notin
2006-09-01	Ajout iter_rel_context/iter_named_context	herbelin
2006-09-01	Appel à caml_modify pour Ocaml 3.07	notin
2006-09-01	Modification du manuel de référence: le flag evar pour cbv n'existe plus.	notin
2006-08-31	Un peu de delta-réduction...	herbelin
2006-08-30	Modification du configure pour paramétrer les exécutables liés à la compi...	notin
2006-08-29	Compilation de Coq sous Windows	notin
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	Changement de l'appel aux exécutables Caml (noms absolus)	notin
2006-08-29	Il faut (au moins) normaliser les evars avant de tenter	herbelin
2006-08-28	Passage à une définition de inhabited plus dans les 'standard mathématique...	herbelin
2006-08-28	improve the amount of information given by the Ltac tactic debugger	bertot
2006-08-28	"Essai de remplacement de "ex P" par "exists x, P x" suite à	herbelin
2006-08-28	MAJ	herbelin
2006-08-28	Ajout thèse Cornes	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