coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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-12
*	Ajout eassumption index	herbelin	2006-09-11
*	Retour à un warning en cas de (co-)fixpoint pas totalement mutuel	herbelin	2006-09-09
*	Updating the doc about Function and co	courtieu	2006-09-07
*	Finalement, interdiction des points fixes non totalement mutuellement	herbelin	2006-09-06
*	Code mort	herbelin	2006-09-05
*	Workaround Map.fold semantic change in ocaml-3.08.4 and higher.	msozeau	2006-09-05
*	Fix wrong order for building library, add informative messages.	msozeau	2006-09-04
*	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-09-01
*	Un peu de delta-réduction...	herbelin	2006-08-31
*	Modification du configure pour paramétrer les exécutables liés à la compi...	notin	2006-08-30
*	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-29
*	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	2006-08-28
*	Export de closedn pour Evarutil	herbelin	2006-08-28
*	Petite optimisation récursive-terminale en passant	herbelin	2006-08-28
*	two minor bug corrections in General Recursive Functions	jforest	2006-08-25
*	correction bug vm_compute	bgregoir	2006-08-25
*	Morceau de code mort	herbelin	2006-08-24
*	Amelioration des messages d'erreur de Fucntion	jforest	2006-08-24