coq - The formal proof system

Age	Commit message (Expand)	Author
2002-12-10	Avertissement plus clair	herbelin
2002-12-10	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin
2002-12-10	maj	filliatr
2002-12-09	Corrections de gestion des univers et modules + meilleure gestions des noms...	coq
2002-12-09	Ajoute le bon traitement pour Ring, Locate, Comments	bertot
2002-12-09	Add an example with Ring.	bertot
2002-12-09	setoids dans noreal	letouzey
2002-12-09	Take notations into account: numbers and the CNotation operator.	bertot
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	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