coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Test Conjecture	herbelin	2003-10-08
*	MAJ	herbelin	2003-10-08
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	Renommage no-strict en -strict-implicit	herbelin	2003-10-08
*	Renommage no-strict en -strict-implicit	herbelin	2003-10-08
*	Renommage no-strict en -strict-implicit; option -dont-load-proofs	herbelin	2003-10-08
*	Mise en place d'un mecanisme ne chargeant pas les preuves opaques	herbelin	2003-10-08
*	maj	filliatr	2003-10-07
*	Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'	herbelin	2003-10-07
*	Debranchement de l'affichage automatique de Proof par le traducteur (trop com...	herbelin	2003-10-07
*	Inspect saute maintenant les marqueurs invisibles	herbelin	2003-10-07
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Compatibilite V7 des noms d'hypotheses	herbelin	2003-10-07
*	Pour rendre make un peu moins verbeux	letouzey	2003-10-06
*	NEWCONTRIBVO doit apparaitre apres CONTRIBVO	herbelin	2003-10-06
*	pour ocamlweb	letouzey	2003-10-06
*	distinguer interp_cs et interp_setcs	letouzey	2003-10-06
*	Debranchement de la regle .v.vo pour que celle-ci ne soit pas prise quand new...	herbelin	2003-10-04