coq - The formal proof system

Age	Commit message (Expand)	Author
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
2006-08-28	Export de closedn pour Evarutil	herbelin
2006-08-28	Petite optimisation récursive-terminale en passant	herbelin
2006-08-25	two minor bug corrections in General Recursive Functions	jforest
2006-08-25	correction bug vm_compute	bgregoir
2006-08-24	Morceau de code mort	herbelin
2006-08-24	Amelioration des messages d'erreur de Fucntion	jforest
2006-08-24	MAJ biblio	herbelin
2006-08-24	MAJ JMeq sur Type + typos (sur propositions de Pierre Castéran)	herbelin
2006-08-24	MAJ biblio	herbelin
2006-08-24	JMeq maintenant applicable sur Type	herbelin
2006-08-23	Bug in replace tactics introduced in r9073 (overlap between replace .. with a...	jforest
2006-08-22	making otags working	jforest
2006-08-22	Forgot a file in previous commit	jforest
2006-08-22	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest
2006-08-22	remove an orphan comment (attached to a piece of code that was removed).	bertot
2006-08-17	Checks that abstract setoid rings can be defined in a module and the tactic	bertot
2006-08-17	corrects an error in the substitution of module paths inside tactics:	bertot