aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
2002-09-29Modifs diversesherbelin
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
2002-09-27Filtrage redondantherbelin
2002-09-27passage a ocaml 3.06herbelin
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
2002-09-27majfilliatr
2002-09-26suppression de l'axiome eqDomdesmettr
2002-09-25preuve d'un axiome restant via Rtopologydesmettr
2002-09-25MAJ pour Rtopologydesmettr
2002-09-25Proprietes topologiques dans Rdesmettr
2002-09-25*** empty log message ***desmettr
2002-09-25Affaiblissement de l'ordre sur Z on demande x < y et seulementmohring
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
2002-09-24Nametab data structure reorganisationcoq
2002-09-24suite chgt liés aux modulesletouzey
2002-09-21Changement de sémantique de Remark : maintenant un global comme les autresherbelin
2002-09-21majfilliatr
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
2002-09-20majfilliatr
2002-09-20majfilliatr
2002-09-20majfilliatr
2002-09-19portage Correctness (substitutivité pour les modules)filliatr
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
2002-09-17echappements incorrects dans chainefilliatr
2002-09-16Réintroduction de l'expansion des variables de shell et de '~' dans lesherbelin
2002-09-16Un peu plus de flexibilité pour la position du '.' finalherbelin
2002-09-16Subst (tout court)filliatr
2002-09-13Ajout contribs manquantesherbelin
2002-09-11tactique Subst x1 ... xnfilliatr
2002-09-09Code mort de AutoRewriteherbelin
2002-09-03Amélioration messages d'erreur non inférence implicitesherbelin
2002-09-03pretyping/pretyping.mlherbelin
2002-08-21Correctioncoq
2002-08-19La notation 'with'. L'interpretation - version preliminairecoq
2002-08-19MAJ .dependcoq
2002-08-19Pretty-printing preliminaire des modules, commandescoq
2002-08-17Suppression automatique du corps des définitions locales opaques dansherbelin
2002-08-16correction de bugs:barras
2002-08-16Encore quelques tests sur modules...coq
2002-08-16Strengthenning rules for modules + No modules in sectionscoq
2002-08-15Test for redundant clausesherbelin
2002-08-14Test affichage optimal des coercionsherbelin
2002-08-14MAJ depend.coqcoq
2002-08-13AutoRewrite substitutive...coq
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
2002-08-13Renoncementherbelin
2002-08-13Petites corrections ici et lacoq
2002-08-13Preuves dans CC deherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-09 14:46:52 +0000