coq - The formal proof system

Age	Commit message (Expand)	Author
2000-12-14	On force l'évaluation du qualid_of_global qui peut échouer dans le débugger	herbelin
2000-12-13	Bug Inversion en présence de méta-variables	herbelin
2000-12-13	conflit useInversionLemma	mohring
2000-12-12	mise a jour	filliatr
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-12-12	* empty log message *	mohring
2000-12-12	Hint Unfold Local + commentaires	mohring
2000-12-12	Ajout de tests	mohring
2000-12-12	petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silent	filliatr
2000-12-12	Reparation Intro sans nom qui ne reduisait pas le but quand celui-ci	mohring
2000-12-11	numarg -> pure_numarg a poursuivre	mohring
2000-12-11	Debut de reparation de simpl	mohring
2000-12-09	tests automatiques	herbelin
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	* empty log message *	sacerdot
2000-12-06	Modif rapide pour prise en compte eqT	herbelin
2000-12-06	Prise en compte `?' dans les `` ``	herbelin
2000-12-06	MAJ nom long de eq	herbelin
2000-12-06	Bug identarg au lieu de qualidarg	herbelin
2000-12-06	section_path etait en fait bonne dans ast et buggee dans printer.ml	herbelin
2000-12-06	* empty log message *	mohring
2000-12-06	2ème bug de traduction des Path	herbelin
2000-12-06	Bug de traduction des Path	herbelin
2000-12-06	message d'erreur	herbelin
2000-12-06	MAJ	herbelin
2000-12-06	Extension de la syntaxe de LetTac	herbelin
2000-12-06	Ajout erreur DoesNotOccurIn	herbelin
2000-12-06	Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...	herbelin
2000-12-06	Notion de 'clause_pattern' pour désigner un ensemble d'occurrences dans le b...	herbelin
2000-12-06	Divers bugs LetTac	herbelin
2000-12-06	Retrait list_except_assoc qui existe en standard dans ocaml (remove_assoc)	herbelin
2000-12-06	* empty log message *	mohring
2000-12-06	* empty log message *	mohring
2000-12-06	* empty log message *	mohring
2000-12-06	* empty log message *	mohring
2000-12-06	Pour la phase debugage	mohring
2000-12-06	Reparation conditions de positivites inductifs, echange dans add_entry	mohring
2000-12-06	Correction pour les qualidconstarg	delahaye
2000-12-05	Reparation d'un bug de pretty-print	delahaye
2000-12-05	Plus de quote devant les ident et les ?	delahaye
2000-12-05	Ajout du répertoire config utilisé par System en local	herbelin
2000-12-05	Bug Cases en presence d'une absence de clause	herbelin
2000-12-05	Prise en compte Let dans le calcul des arguments manquants d'un lemme (clenv_...	herbelin
2000-12-05	Inner types are now reduced and arrows are created when	sacerdot
2000-12-05	MAJ	herbelin
2000-12-05	Mini-nettoyage noms longs	herbelin
2000-12-05	Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de l...	herbelin
2000-12-05	Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de l...	herbelin
2000-12-04	caractere opaque des constantes repris en compte	filliatr