coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	module Library	filliatr	1999-09-18
*	affichage des erreurs de typage dans minicoq	filliatr	1999-09-10
*	modules System, Lib et States	filliatr	1999-09-10
*	les sections ne sont plus stockées à l'envers dans les section paths	filliatr	1999-09-09
*	- deplacement time stamps dans System (car utilise Unix)	filliatr	1999-09-08
*	- bug: une fois typés, les arités des constructeurs étaient rangées	filliatr	1999-09-07
*	- minicoq : definition inductifs; syntaxe a->b	filliatr	1999-09-07
*	mise en place commandes minicoq	filliatr	1999-09-07
*	mise en place repertoire test-suite/, toplevel/, parsing/	filliatr	1999-09-06
*	modules Libobject et Summary (partiel)	filliatr	1999-09-03
*	- environnements vides	filliatr	1999-09-03
*	typage constructeur :	filliatr	1999-08-30
*	ajout des inductifs (sans types singletons pour l'instant)	filliatr	1999-08-30
*	un petit effort de presentation dans les interfaces	filliatr	1999-08-30
*	suppression champs inutiles dans constantes et inductifs; verification defini...	filliatr	1999-08-27
*	environnement sur	filliatr	1999-08-26
*	mach -> typing; machops -> typeops	filliatr	1999-08-26
*	- abstraction	filliatr	1999-08-26
*	modules Instantiate, Constant et Inductive	filliatr	1999-08-25
*	mach et himsg; typage sans extraction	filliatr	1999-08-24
*	- suppression de CONV_X et CONV_X_LEQ : les univers sont maintenant toujours	filliatr	1999-08-23
*	programmation literaire : un fichier de description par repertoire	filliatr	1999-08-20
*	machine: execute = typage avec univers	filliatr	1999-08-20
*	mise en place programmation literaire (generation de doc/coq.tex)	filliatr	1999-08-19
*	module Reduction (fin)	filliatr	1999-08-18
*	module Reduction (debut)	filliatr	1999-08-18
*	module Closure	filliatr	1999-08-17
*	generic, term et evd	filliatr	1999-08-17
*	ancien names decoupe en names + sign	filliatr	1999-08-16
*	Initial revision	filliatr	1999-08-16