coq - The formal proof system

Age	Commit message (Expand)	Author
2001-08-10	Parsing	herbelin
2001-08-10	Repository : pauillac.inria.fr:/net/pauillac/constr/ARCHIVE	herbelin
2001-08-08	Renommage TrueCut -> Assert	herbelin
2001-08-08	Ajout nf_betaiota dans le cut interne	herbelin
2001-08-08	La grammaire n'était plus LL1	herbelin
2001-08-08	Modification Tauto pour qu'il puisse destructurer des hypotheses de la forme	courant
2001-08-07	Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...	herbelin
2001-08-07	Passage au nouveau Destruct	herbelin
2001-08-06	Nouvelle entrée ident_or_numarg	herbelin
2001-08-05	Expérimentation de NewDestruct et parfois NewInduction	herbelin
2001-08-05	Code mort	herbelin
2001-08-05	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin
2001-08-05	Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...	herbelin
2001-08-05	Ajout error_global_not_found	herbelin
2001-08-05	Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...	herbelin
2001-08-05	Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction	herbelin
2001-08-05	Suppression des TmpHyp disgracieuses dans Decompose; utilisation de combinate...	herbelin
2001-08-05	Elimination des coupures quand les 'clause' se réduisent à des hypothèses,...	herbelin
2001-08-05	Nouveau profiler compatible avec ocaml >= 3.01	herbelin
2001-08-01	Ajout code pour un Destruct similaire au NewInduction	herbelin
2001-08-01	Ajout make_elimination_ident	herbelin
2001-08-01	Ajout add_prefix/add_suffix	herbelin
2001-08-01	Ajout profile dans PARSERREQUIRE, nécessaire si certaines fonctions d'un des...	herbelin
2001-08-01	MAJ vis à vis de ocaml 3.01	herbelin
2001-07-24	Suppression de l'affichage du non-reparsable 'Local constraint change'	herbelin
2001-07-24	Bug Simpl	herbelin
2001-07-23	Comentaire errone.	clrenard
2001-07-21	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin
2001-07-21	Nettoyage	herbelin
2001-07-21	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin
2001-07-19	Changements dans le traitement des qualid's	delahaye
2001-07-19	modifs de preuves (plus simples)	mayero
2001-07-18	Ajout de la contrib sur les graphes	mohring
2001-07-17	"make clean" nettoie les .g all.ps all-gal.ps et les fichiers HTML	filliatr
2001-07-16	all.g.ps -> all-gal.ps	filliatr
2001-07-16	compat -sort et -suffix	filliatr
2001-07-16	cibles all.ps et all-gal.ps (utilisation de coqweb)	filliatr
2001-07-16	utilisation de printf (simplif)	filliatr
2001-07-16	modif Map section	mohring
2001-07-16	Nettoyage	mohring
2001-07-13	reparation regles pour parsing Coercion Local	mohring
2001-07-13	Branchement de induction/destruct sur intros_until_n (intros_do obsolete ne p...	herbelin
2001-07-10	Setoid_rewrite -> Rewrite	clrenard
2001-07-10	Branchement sur bad_tactic_args	herbelin
2001-07-10	Branchement sur bad_tactic_args	herbelin
2001-07-10	Ajout des fichiers pour le Ring pour setoides	clrenard
2001-07-10	Ajout du .ml pour la tactique Setoid_replace	clrenard
2001-07-10	Ajout du .v pour la tactique Setoid_replace	clrenard
2001-07-10	Changement de place de la tactique Setoid_rewrite et renommage	clrenard
2001-07-10	Changement de place de la tactique Setoid_rewrite	clrenard