aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-09-14Transformation de Remark/Fact en constantes non visibles sans qualificationherbelin
2001-09-14Ajout syntaxe "Assert H:T."herbelin
2001-09-14L'instantiation des evars quand un produit ou une sorte Ă©taient attendus n'Ă...herbelin
2001-09-14L'instantiation des evars quand un produit ou une sorte Ă©taient attendus n'Ă...herbelin
2001-09-14exceptionsbarras
2001-09-14mauvais rattrapage d'exceptionbarras
2001-09-13Only CHANGES !herbelin
2001-09-13Structuration et traductionherbelin
2001-09-13Prise en compte qualid dans Hint Unfoldherbelin
2001-09-13Syntaxe des Hintsherbelin
2001-09-13uniformité des cibles pour les contribsfilliatr
2001-09-13mise Ă  jourfilliatr
2001-09-13eclaircissement du codecourant
2001-09-13explications modifications Tautocourant
2001-09-12*** empty log message ***mohring
2001-09-12Rustine pour gérer inject_natherbelin
2001-09-11Un look un peu plus avenant aux productions des règles de grammaireherbelin
2001-09-11Du bon usage des commentaires coqwebherbelin
2001-09-11Conformité des commentaires au format coqwebherbelin
2001-09-11MAJherbelin
2001-09-10Hack pour gérer les univers dans les prédicats de Cases synthétisésherbelin
2001-09-10changement du make depend en vu du make realsletouzey
2001-09-10bug de rename_global modulaire corrige'letouzey
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-09-10Un conv aurait dĂ» ĂŞtre un conv_leqherbelin
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-09-09Légère modification lookup_eliminatorherbelin
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-09-09Amélioration check_module_nameherbelin
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
2001-09-09Suppression de Type_1, inutile, et non prévu dans le modèle des univers alg...herbelin
2001-09-09Préparation du prétypage à la mise en place d'univers algébriquesherbelin
2001-09-09MĂ©canisme pour faire remonter les contraintes de typage sur les variables de...herbelin
2001-09-09MĂ©canisme pour faire remonter les contraintes de typage sur les variables de...herbelin
2001-09-09Suppression du retypage dans w_Declareherbelin
2001-09-09MAJherbelin
2001-09-09Tests l'incohérence des universherbelin
2001-09-08MAJherbelin
2001-09-07MAJherbelin
2001-09-07Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)herbelin
2001-09-07Suppression des library roots, on teste si un nom est absolu autrementherbelin
2001-09-06RĂ©tablissement de Print Sectionherbelin
2001-09-06MAJherbelin
2001-09-06Bug default module name (2eme)herbelin
2001-09-06Bug default module nameherbelin
2001-09-05Version de la reduction dans Closure plus econome en memoire:barras
2001-09-04Nouveau coq.spec avec les droits de rootherbelin
2001-09-04erreur de pretty-print lors de l'affichage de termes avec de Bruijn non liesbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-21 03:00:21 +0000