coq - The formal proof system

Age	Commit message (Expand)	Author
2001-03-12	fin du letin	letouzey
2001-03-12	debut let in	filliatr
2001-03-12	mise a jour commentaires'	filliatr
2001-03-12	Commentaires. Verification des assert false. Probleme des types ML arity.	letouzey
2001-03-07	distinction contexte et signature	filliatr
2001-03-06	plus de commentaires	letouzey
2001-03-05	ocamlweb	filliatr
2001-03-05	extraction termes (suite)	filliatr
2001-03-05	indentation code	filliatr
2001-03-01	De bizarres SR_pus_assoc au lieu de SR_plus_assoc	herbelin
2001-03-01	Déplacement de qualid dans Nametab, hors du noyau	herbelin
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-27	debut extraction termes; pp lambda	filliatr
2001-02-26	ajout Vprop, Tprop et Eprop	filliatr
2001-02-22	extraction des types et des inductifs	filliatr
2001-02-21	nouveau design ou le renommage sera fait a posteriori	filliatr
2001-02-20	mise en place fichiers extraction	filliatr
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-02-14	Renommage des variables dans les schémas d'induction	herbelin
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2001-02-13	Absolute URL for DTDs introduced	sacerdot
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-02-06	mise en place extraction	filliatr
2001-02-05	rétablissement patch Claudio	filliatr
2001-02-02	retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...	filliatr
2001-02-01	- coqc : option -image	filliatr
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2001-01-12	Now Ring does not perform any more the same reduction twice.	sacerdot
2001-01-12	Comment fixed	sacerdot
2001-01-11	Now reduction to normal form is done only when the term is not	sacerdot
2001-01-11	Many unuseful rewritings are no more done by Ring.	sacerdot
2001-01-11	Mise a jour Rbase	mohring
2001-01-09	Meta Definition -> Tactic Definition	delahaye
2001-01-09	Tactic Definition -> Meta Definition	delahaye
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-20	Scripts de correction d'uri	herbelin
2000-12-20	MAJ	herbelin
2000-12-20	Non verbose par défaut	herbelin
2000-12-14	Bug sur commit précédent	herbelin
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-07	type attribute added to PROD (for ForAll vs Pi rendering)	sacerdot
2000-12-07	COPYRIGHT file added; some comments changed	sacerdot
2000-12-06	Bug identarg au lieu de qualidarg	herbelin
2000-12-05	Inner types are now reduced and arrows are created when	sacerdot
2000-12-01	LETIN now has a letintarget instead of a target	sacerdot
2000-12-01	cictypes.dtd changed	sacerdot
2000-11-30	Used a force function to force stream evaluation only for aestaetics reasons.	sacerdot