coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)	herbelin	2003-11-17
*	Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar	herbelin	2003-11-15
*	Ajout Print Implicit avec depliage du type	herbelin	2003-11-15
*	Compatibilite %T	herbelin	2003-11-14
*	Bug parsing cast	herbelin	2003-11-14
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Suppression du "..." final !	herbelin	2003-11-12
*	Mise en place systeme de renommage des noms de variables liees dans la biblio...	herbelin	2003-11-12
*	MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter l...	herbelin	2003-11-12
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
*	petits changements de syntaxe	barras	2003-11-12
*	Suppression SearchNamed finalement redondant avec SearchAbout	herbelin	2003-11-10
*	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin	2003-11-09
*	'as' avant 'using' dans 'destruct'	herbelin	2003-11-09
*	Fusion de tuple_constr/tuple_pattern dans operconstr/pattern	herbelin	2003-11-08
*	Added Instantiate ... in	corbinea	2003-11-06
*	Interpretation des entiers dans N (ex-entier), maj du module des positive	herbelin	2003-11-05
*	En v8, une notation, c'est 2 regles et un niveau	herbelin	2003-11-04
*	Explicitation message d'erreur nombres negatifs	herbelin	2003-11-04
*	Compatibilite V7.4 pour le delimiteur de positive	herbelin	2003-11-03
*	Le printeur de Show Script n'etait pas le bon en v7	herbelin	2003-11-02
*	Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8	herbelin	2003-11-01
*	Il ne faut pas mettre le constrarg des tactiques au niveau lconstr	herbelin	2003-11-01
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Traduction des noms pour les refs de pr_glob_generic (via pr_global)	herbelin	2003-11-01
*	Utilisation de niveaux pour l'extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	Extension de get_constr_entry et symbol_of_production pour gerer les extensio...	herbelin	2003-11-01
*	Heritage des notations v7 seulement si zero information v8	herbelin	2003-11-01
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30
*	Ajout de Print Visibility	herbelin	2003-10-28
*	Saut de ligne avant les infos non logiques de print_about	herbelin	2003-10-23
*	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin	2003-10-23
*	Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition	herbelin	2003-10-23
*	Independance de grammar.cmo vis a vis de Search	herbelin	2003-10-23
*	Suppression dependance formelle en Vernacexpr	herbelin	2003-10-22
*	Integration de SearchNamed dans SearchAbout	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...	herbelin	2003-10-21
*	Extension de Locate	herbelin	2003-10-21
*	On n'autorise plus les niveaux doubles L/R en v8	herbelin	2003-10-17
*	Bug mot-cle TYPES	herbelin	2003-10-17
*	Traduction des idents aussi dans le printer generique des tactiques	herbelin	2003-10-17
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	lettac -> set	barras	2003-10-16
*	Bug Search	herbelin	2003-10-16
*	Mise en conformite return_type en fonction de la doc	herbelin	2003-10-15
*	Changement 'as notation' en 'where notation'	herbelin	2003-10-14
*	Ameliration affichage inductifs	herbelin	2003-10-13
*	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin	2003-10-13