coq - The formal proof system

Age	Commit message (Expand)	Author
2001-12-19	Insertion unification non seulement en tête mais à l'intérieur des motifs ...	herbelin
2001-12-19	reparation de make doc (ocamlweb & _)	letouzey
2001-12-18	the function Ctast.section_path was wrong. It performed two reverse	bertot
2001-12-18	Pour ocamlweb ...	letouzey
2001-12-18	Oubli d'un quote	herbelin
2001-12-18	On ne peut plus appliquer des arguments à une syntaxe primitive	herbelin
2001-12-18	There remained traces of streams with the old syntax.	bertot
2001-12-18	Add a new file in the files needed for the "coq-interface" binary: the file	bertot
2001-12-18	Add dependencies for two new files in contrib/interface	bertot
2001-12-18	Integrating the Ltac language and the Blast tool into the interface	bertot
2001-12-18	affichage correct du type des inductifs et constructeurs en presence	barras
2001-12-18	typo de parenthèsage + suppression de string (= str maintenant)	letouzey
2001-12-18	anti revolution culturelle: retour des arguments logiques	letouzey
2001-12-18	ote les redondances des entetes	letouzey
2001-12-18	coq-bugs #12: probleme de metamap resolu	barras
2001-12-18	MAJ	herbelin
2001-12-18	parsing des branches de Cases au niveau lconstr (au lieu de constr)	barras
2001-12-18	Grossière erreur de typage	herbelin
2001-12-18	Nettoyage exceptions liées au vieux Case	herbelin
2001-12-18	Nettoyage exceptions liées au vieux Case; réparation du try with UserError ...	herbelin
2001-12-17	Mauvais nom d'erreur d'échec de nth	herbelin
2001-12-17	probleme des Require dans les sections	barras
2001-12-17	le save de Correctness faisant assert false	barras
2001-12-16	Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...	herbelin
2001-12-13	MAJ	herbelin
2001-12-13	* empty log message *	herbelin
2001-12-13	MAJ de la traduction en ast des variables de section en qualid	herbelin
2001-12-13	Contournement du problème des evars de type, typées par défaut dans Type (...	herbelin
2001-12-13	Affichage NewInduction/NewDesctruct	herbelin
2001-12-13	Contournement du problème des evars de type, typées par défaut dans Type	herbelin
2001-12-13	package Debian 7.1, correction pb compilation native sur certaines architectures	courant
2001-12-13	compat ocaml 3.03	filliatr
2001-12-12	MAJ	herbelin
2001-12-11	suppression de l'affichage des noeuds Change_evars	barras
2001-12-11	* empty log message *	courant
2001-12-11	ajout du document sur la nouvelle syntaxe	barras
2001-12-11	document sur les propositions de nouvelle syntaxe	barras
2001-12-11	Mise en place de coercion dans les motifs	herbelin
2001-12-11	Test des coercions dans les motifs	herbelin
2001-12-10	- condition de garde (suite)	barras
2001-12-10	correction de bugs concernant la gestion des modules. debranchement du test d...	letouzey
2001-12-10	mise a jour	filliatr
2001-12-07	* empty log message *	desmettr
2001-12-07	* empty log message *	desmettr
2001-12-06	Maj	herbelin
2001-12-06	Parade contre effet indésirable du commit précédent	herbelin
2001-12-06	Affichage des '_' pour Intros	herbelin
2001-12-06	Amélioration nommage hypothèses NewInduction (et incompatibilités)	herbelin
2001-12-05	* empty log message *	desmettr
2001-12-05	* empty log message *	desmettr