coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-27	Ajout ne_string	herbelin
2003-11-26	Protection contre les notations vides	herbelin
2003-11-26	Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...	herbelin
2003-11-25	modif lexer: ident peut commencer par _	barras
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-23	Prise en compte des definitions locales dans les (co-)points-fixes	herbelin
2003-11-21	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-20	Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...	herbelin
2003-11-19	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-18	reparation bug moins unaire (erreur de PP)	barras
2003-11-18	Code mort	herbelin
2003-11-17	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-15	Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar	herbelin
2003-11-15	Ajout Print Implicit avec depliage du type	herbelin
2003-11-14	Compatibilite %T	herbelin
2003-11-14	Bug parsing cast	herbelin
2003-11-13	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras
2003-11-13	factorisation et generalisation des clauses	barras
2003-11-12	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-10	Suppression SearchNamed finalement redondant avec SearchAbout	herbelin
2003-11-09	Traduction semantique des InHyp de clause en InHypValue si local def	herbelin
2003-11-09	'as' avant 'using' dans 'destruct'	herbelin
2003-11-08	Fusion de tuple_constr/tuple_pattern dans operconstr/pattern	herbelin
2003-11-06	Added Instantiate ... in	corbinea
2003-11-05	Interpretation des entiers dans N (ex-entier), maj du module des positive	herbelin
2003-11-04	En v8, une notation, c'est 2 regles et un niveau	herbelin
2003-11-04	Explicitation message d'erreur nombres negatifs	herbelin
2003-11-03	Compatibilite V7.4 pour le delimiteur de positive	herbelin
2003-11-02	Le printeur de Show Script n'etait pas le bon en v7	herbelin
2003-11-01	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-10-30	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin
2003-10-28	Ajout de Print Visibility	herbelin
2003-10-23	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