coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bug affichage Decompose	herbelin	2003-12-24
*	* empty log message *	barras	2003-12-23
*	Mise en valeur intropattern de paires et acceptation dans le 'as' de inductio...	herbelin	2003-12-22
*	Substitution dans REvar et PEvar plutot que encodage via noeud application po...	herbelin	2003-12-19
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
*	ajout test de non-regression Clear d'une def locale	barras	2003-12-17
*	MAJ suppression 250	herbelin	2003-12-16
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	correction bug: parentheses ne cassent plus les implicites	barras	2003-12-08
*	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin	2003-12-04
*	Symetrisation parsing/printing 'abstract'	herbelin	2003-12-04
*	Nouvelle tactique EExists	clrenard	2003-12-01
*	Ajout ne_string	herbelin	2003-11-27
*	Protection contre les notations vides	herbelin	2003-11-26
*	Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...	herbelin	2003-11-26
*	modif lexer: ident peut commencer par _	barras	2003-11-25
*	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin	2003-11-25
*	Prise en compte des definitions locales dans les (co-)points-fixes	herbelin	2003-11-23
*	Suppression des niveaux vides	herbelin	2003-11-21
*	Ajout Print Implicit	herbelin	2003-11-21
*	Pas d'entrees autres que les predefinies en v8	herbelin	2003-11-21
*	Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...	herbelin	2003-11-20
*	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...	herbelin	2003-11-19
*	Protection contre l'effacement des niveaux vides de operconstr et pattern par...	herbelin	2003-11-19
*	reparation bug moins unaire (erreur de PP)	barras	2003-11-18
*	Code mort	herbelin	2003-11-18
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
*	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