coq - The formal proof system

Age	Commit message (Expand)	Author
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
2006-08-16	+ timide essai pour le traitement des as dans les patterns lors de la generat...	jforest
2006-08-16	MAJ Rectutorial (P. Castéran)	notin
2006-08-15	working on functional induction automation (tactic finduction and	courtieu
2006-08-14	comparison functions should be Defined not Qed	letouzey
2006-08-11	Bug corrections in Function.	jforest
2006-08-08	In the old version, recursive functions cannot be declared inside a section	bertot
2006-07-28	Modifications dans les scripts de configuration (coqtop et coqide affichent m...	notin
2006-07-28	MAJ de la biblio du manuel de référence	notin
2006-07-28	Reparation bug Show intros: les hypothèses introduites précédemment	courtieu
2006-07-27	Correction du bug #1170: les options synchronisées déclarées dans une sect...	notin
2006-07-26	Modification script sed pour compatibilité Windows	notin
2006-07-22	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir