coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	quelques trucs necessaires au toplevel	filliatr	1999-09-28
*	retablissement du toplevel	filliatr	1999-09-28
*	ajout de divers fonctions dans lib/	filliatr	1999-09-28
*	ajout des constraintes pendant le chargement d'un module (load)	filliatr	1999-09-27
*	report d'une correction de Bruno	filliatr	1999-09-27
*	message erreur UI pendant import	filliatr	1999-09-26
*	ensembles de contraintes d'univers	filliatr	1999-09-25
*	module Declare	filliatr	1999-09-19
*	- un effort sur la doc (ocamlweb)	filliatr	1999-09-19
*	un effort sur la doc (ocamlweb)	filliatr	1999-09-19
*	module Library	filliatr	1999-09-18
*	affichage des erreurs de typage dans minicoq	filliatr	1999-09-10
*	documentation repertoire toplevel	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
*	simplifications de code	filliatr	1999-09-09
*	implode codé avec String.concat	filliatr	1999-09-09
*	environement global	filliatr	1999-09-09
*	compilation en natif (règles génériques, cibles coqtop et coqtop.byte, etc.)	filliatr	1999-09-09
*	module Himsg	filliatr	1999-09-08
*	module Himsg, comme un foncteur	filliatr	1999-09-08
*	cible doc	filliatr	1999-09-08
*	on fabrique aussi dev/db_printer.cmo	filliatr	1999-09-08
*	un wrapper autour de ocamldebug	filliatr	1999-09-08
*	printers pour le debugger	filliatr	1999-09-08
*	le bien nomme'	filliatr	1999-09-08
*	changements dans les grammaires	filliatr	1999-09-08
*	compilation des grammaires (ouf)	filliatr	1999-09-08
*	- deplacement time stamps dans System (car utilise Unix)	filliatr	1999-09-08
*	modules grammaire Coq	filliatr	1999-09-08
*	time stamps dans System	filliatr	1999-09-08
*	modules Ast et Pcoq	filliatr	1999-09-08
*	deplacement coqast vers parsing/	filliatr	1999-09-08
*	minicoq: pretty-print applications; ambiguite grammaire supprimee; Ind, Const...	filliatr	1999-09-08
*	fichier de test d'inductifs pour minicoq	filliatr	1999-09-08
*	fichiers camlp4 avec suffix .ml4	filliatr	1999-09-08
*	doc minicoq (grammaires)	filliatr	1999-09-07
*	mise a jour	filliatr	1999-09-07
*	pretty-print A->B	filliatr	1999-09-07
*	instanciation des opérateurs sur la bonne signature (celle de	filliatr	1999-09-07
*	- 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
*	(debut) de grammaire minicoq	filliatr	1999-09-07
*	mise en place grammaire minicoq	filliatr	1999-09-07
*	mise en place repertoire test-suite/, toplevel/, parsing/	filliatr	1999-09-06
*	un mini toplevel pour tester le noyau	filliatr	1999-09-06
*	debut d'un lexer	filliatr	1999-09-06
*	modules Libobject et Summary (partiel)	filliatr	1999-09-03
*	- environnements vides	filliatr	1999-09-03