coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	mise a jour nouvelle syntaxe	barras	2003-10-11
*	maj	filliatr	2003-10-10
*	Suppression Grammar/Syntax	herbelin	2003-10-10
*	identity est equivalent sur Type (sauf sans argument)	herbelin	2003-10-10
*	nat_scope ouvert par defaut	herbelin	2003-10-10
*	identity est equivalent sur Type (sauf sans argument)	herbelin	2003-10-10
*	type_scope	herbelin	2003-10-10
*	Suppression de definitions equivalentes	herbelin	2003-10-10
*	Bug undo	herbelin	2003-10-10
*	Notation '^'	herbelin	2003-10-10
*	* empty log message *	herbelin	2003-10-10
*	Plus d'Eval Compute	herbelin	2003-10-10
*	MAJ commentaires	herbelin	2003-10-10
*	MAJ	herbelin	2003-10-10
*	Typo	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Delimiters N devient 'nat'	herbelin	2003-10-10
*	Cablage en dur de inversion	herbelin	2003-10-10
*	code mort	herbelin	2003-10-10
*	show_subgoals dans Pfedit	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	MAJ .v8	herbelin	2003-10-10
*	pf_get_new_id en provenance de feu wcclausenv	herbelin	2003-10-10
*	Suppression clenv_change_head que seul Wcclausenv utisait	herbelin	2003-10-10
*	Dead of 'a somewhat cryptic module'	herbelin	2003-10-10
*	Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...	herbelin	2003-10-10
*	Ajout printers pour constr et constr_pattern (sans traduction)	herbelin	2003-10-10
*	Unification lemInv et lemInv_in	herbelin	2003-10-10
*	pr_tactic sans traduction; affichage Inversion	herbelin	2003-10-10
*	Cablage en dur de inversion	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Intégration de la premiere partie de 'hightactics' dans 'tactics' suite à c...	herbelin	2003-10-10
*	Affichage des buts par Pfedit pour utilisation par les tactiques	herbelin	2003-10-10
*	Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...	herbelin	2003-10-10
*	Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...	herbelin	2003-10-10
*	Gestion en temps constant de la pile des Unfo	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Cacher les .v8	herbelin	2003-10-10
*	Renommage en v8 de PolyList en List et List en MonoList	herbelin	2003-10-10
*	Renommage en v8 de PolyList en List et List en MonoList	herbelin	2003-10-10
*	Nouveau format de l'option 'format'	herbelin	2003-10-09
*	Compatibilite ocaml 3.06 et 3.07	herbelin	2003-10-09
*	Syntaxe VernacEndProof changee pour ajout mot-cle 'Admitted'	herbelin	2003-10-09
*	Teste interaction ltac et modules	herbelin	2003-10-08
*	Ajout exemple parametres implicites	herbelin	2003-10-08
*	Bug utilisation nametab pour ltac	herbelin	2003-10-08
*	Pb residuel avec la prise en compte des parametres implicites d'inductifs	herbelin	2003-10-08
*	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin	2003-10-08
*	Des abbreviations pour constrintern.ml; generic argument IdentArg	herbelin	2003-10-08
*	Des abbreviations pour constrintern.ml	herbelin	2003-10-08