coq - The formal proof system

Age	Commit message (Expand)	Author
2002-12-09	Problèmes et améliorations divers affichage	herbelin
2002-12-09	Essai suppression nf_betaiota dans type_of	herbelin
2002-12-09	Nouvelle preuve de times_convert pour nouvelle définition de times	herbelin
2002-12-09	Problèmes et améliorations affichage; Changement Simpl	herbelin
2002-12-09	Problèmes et améliorations divers affichage	herbelin
2002-12-09	Option pour rendre les vérifications du refiner optionnelle	herbelin
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-12-09	Code mort ?	herbelin
2002-12-09	pp	letouzey
2002-12-09	petit bug	letouzey
2002-12-09	chamboulement du codage des indcutifs extraits; deplacements des tables; ...	letouzey
2002-12-07	Compatibilité times1	herbelin
2002-12-06	Un axiome en attendant la mise a jour de la preuve de times_convert	herbelin
2002-12-06	Amélioration sensible de l'efficacité de Zmult et times	herbelin
2002-12-06	Amélioration sensible de l'efficacité de la multiplication	herbelin
2002-12-06	maj	filliatr
2002-12-05	Ajout affichage fconstr	herbelin
2002-12-05	reorganisation des recherches de ref dans ml_decl	letouzey
2002-12-05	code cleanup (+ debut de commencement de modules)	letouzey
2002-12-05	des Set et des Map en plus	letouzey
2002-12-04	Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...	herbelin
2002-12-04	Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...	herbelin
2002-12-04	Modification Require From	mohring
2002-12-04	Correction d'un message d'erreur de l'application de non-foncteur	coq
2002-12-04	mdule --> module	mohring
2002-12-04	suppression du champ mind_singl inutilisé dans mutual_inductive_body	letouzey
2002-12-04	Corrige un bug de composition de substitutions	coq
2002-12-04	fichiers DOS	filliatr
2002-12-04	maj	filliatr
2002-12-03	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey
2002-12-03	MAJ travail moulinette	herbelin
2002-12-03	bug de non-indépendance des règles d'affichage et parsing vis à vis du nom...	herbelin
2002-12-03	bugs d'affichage (confusion key/scope dans les délimiteurs)	herbelin
2002-12-03	Préparation à la prise en compte des changements de scopes internes aux not...	herbelin
2002-12-03	MAJ	herbelin
2002-12-03	Essai d'introduction d'un scope des types	herbelin
2002-12-03	Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles	bertot
2002-12-03	Pas de globalisation impérative pour les Grammar	herbelin
2002-12-03	Calcul de l'associativité même pour les Grammar avec plusieurs clauses	herbelin
2002-12-03	Le '.' peut faire partie d'un token	herbelin
2002-12-03	maj	filliatr
2002-12-02	Remplacement Grammar par Notation	herbelin
2002-12-02	MAJ sur MAJ	herbelin
2002-12-02	Remplacement de Syntactic Definition par Notation	herbelin
2002-12-02	Associativité de constr9 et lconst à RIGHTA qui est le plus courant	herbelin
2002-12-02	Ajout des options "Set Contextual Implicits" et "Set Strict Implicits	herbelin
2002-12-02	Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation ...	herbelin
2002-12-02	Ajout des options "Set Contextual Implicits" et "Set Strict Implicits	herbelin
2002-12-02	Re-déplacement du résultat de Grammar au niveau constr_expr	herbelin
2002-12-02	Z_scope doit annuler l'affichage de = entre	herbelin